diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Chalice/src | |
Initial set of files.
Diffstat (limited to 'Chalice/src')
| -rw-r--r-- | Chalice/src/Ast.scala | 384 | ||||
| -rw-r--r-- | Chalice/src/Boogie.scala | 270 | ||||
| -rw-r--r-- | Chalice/src/Chalice.cs | 76 | ||||
| -rw-r--r-- | Chalice/src/Chalice.scala | 115 | ||||
| -rw-r--r-- | Chalice/src/ChaliceToCSharp.scala | 211 | ||||
| -rw-r--r-- | Chalice/src/Parser.scala | 409 | ||||
| -rw-r--r-- | Chalice/src/Prelude.scala | 251 | ||||
| -rw-r--r-- | Chalice/src/PrettyPrinter.scala | 292 | ||||
| -rw-r--r-- | Chalice/src/Resolver.scala | 940 | ||||
| -rw-r--r-- | Chalice/src/Translator.scala | 2260 |
10 files changed, 5208 insertions, 0 deletions
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala new file mode 100644 index 00000000..44d97290 --- /dev/null +++ b/Chalice/src/Ast.scala @@ -0,0 +1,384 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+import scala.util.parsing.input.Position
+import scala.util.parsing.input.Positional
+
+trait ASTNode extends Positional
+
+// classes and types
+
+sealed case class Class(id: String, parameters: List[Class], module: String, members: List[Member]) extends ASTNode {
+ var mm = Map[String,Member]()
+ def LookupMember(id: String): Option[Member] = {
+ if (mm.keys exists { i => i.equals(id)})
+ Some(mm(id))
+ else if (IsRef && (RootClass.mm contains id)) {
+ val m = RootClass.mm(id)
+ if (m.Hidden) None else Some(m)
+ } else
+ None
+ }
+ def IsInt: boolean = false
+ def IsBool: boolean = false
+ def IsRef: boolean = true
+ def IsNull: boolean = false
+ def IsMu: boolean = false
+ def IsSeq: boolean = false
+ def IsToken: boolean = false
+ def IsState: boolean = false
+ def IsNormalClass = true;
+ var IsExternal = false; // says whether or not to compile the class (compilation ignores external classes)
+
+ def Fields: List[Field] = {
+ members flatMap (m => m match { case f:Field => List(f) case _ => List() })
+ }
+ def Invariants: List[MonitorInvariant] = {
+ (members :\ List[MonitorInvariant]()) { (m,list) => m match {
+ case m:MonitorInvariant => m :: list
+ case _ => list }}
+ }
+ def FullName: String = if(parameters.isEmpty) id else id + "<" + parameters.tail.foldLeft(parameters.head.FullName){(a, b) => a + ", " + b.FullName} + ">"
+}
+
+case class SeqClass(parameter: Class) extends Class("seq", List(parameter), "default", Nil) {
+ override def IsRef = false;
+ override def IsSeq = true;
+ override def IsNormalClass = false;
+}
+object IntClass extends Class("int", Nil, "default", Nil) {
+ override def IsRef = false
+ override def IsInt = true
+ override def IsNormalClass = false;
+}
+object BoolClass extends Class("bool", Nil, "default", Nil) {
+ override def IsRef = false
+ override def IsBool = true
+ override def IsNormalClass = false;
+}
+object NullClass extends Class("null", Nil, "default", Nil) {
+ override def IsNull = true
+ override def IsNormalClass = false;
+}
+object MuClass extends Class("$Mu", Nil, "default", Nil) {
+ override def IsRef = false
+ override def IsMu = true
+ override def IsNormalClass = false;
+}
+case class TokenClass(c: Type, m: String) extends Class("token", Nil, "default", List(
+ new SpecialField("joinable", new Type(BoolClass))
+))
+{
+ var method = null: Method;
+ override def IsRef = true;
+ override def IsToken = true;
+ override def IsNormalClass = false;
+ override def FullName: String = "token<" + c.FullName + "." + m + ">"
+ mm = mm.+(("joinable", Fields(0)));
+}
+
+object RootClass extends Class("$root", Nil, "default", List(
+ new SpecialField("mu", new Type(MuClass)),
+ new SpecialField("held", new Type(BoolClass)){ override val Hidden = true },
+ new SpecialField("rdheld", new Type(BoolClass)){ override val Hidden = true }
+ )) // joinable and held are bool in Chalice, but translated into an int in Boogie
+{
+ def MentionableFields = Fields filter {fld => fld.id != "held" && fld.id != "rdheld"}
+}
+
+sealed case class Type(id: String, params: List[Type]) extends ASTNode { // denotes the use of a type
+ var typ: Class = null
+ def this(id: String) = { this(id, Nil); }
+ def this(cl: Class) = { this(cl.id); typ = cl }
+ def FullName: String = if(params.isEmpty) id else id + "<" + params.tail.foldLeft(params.head.FullName){(a, b) => a + ", " + b.FullName} + ">"
+}
+
+sealed case class TokenType(C: Type, m: String) extends Type("token", Nil) { // denotes the use of a type
+ typ = TokenClass(C, m);
+ var method = null : Method;
+
+ override def FullName: String = "token<" + C.FullName + "." + m + ">"
+}
+
+// members
+
+sealed abstract class Member extends ASTNode {
+ val Hidden: boolean = false // hidden means not mentionable in source
+}
+case class MonitorInvariant(e: Expression) extends Member
+sealed abstract class NamedMember(id: String) extends Member {
+ val Id = id
+ var Parent: Class = null
+ def FullName = Parent.id + "." + Id
+}
+case class Field(id: String, typ: Type) extends NamedMember(id) {
+ val IsGhost: boolean = false
+}
+case class SpecialField(name: String, tp: Type) extends Field(name, tp) { // direct assignments are not allowed to a SpecialField
+ override def FullName = id
+}
+case class Method(id: String, ins: List[Variable], outs: List[Variable], spec: List[Specification], body: List[Statement]) extends NamedMember(id)
+case class Predicate(id: String, definition: Expression) extends NamedMember(id)
+case class Function(id: String, ins: List[Variable], out: Type, spec: List[Specification], definition: Expression) extends NamedMember(id) {
+ def apply(rec: Expression, args: List[Expression]): FunctionApplication = {
+ val result = FunctionApplication(rec, id, args);
+ result.f = this;
+ result
+ }
+}
+class Variable(name: String, typ: Type) extends ASTNode {
+ val id = name
+ val t = typ
+ val IsGhost: boolean = false
+ val IsImmutable: boolean = false
+ val UniqueName = {
+ val n = S_Variable.VariableCount
+ S_Variable.VariableCount = S_Variable.VariableCount + 1
+ name + "#" + n
+ }
+}
+object S_Variable { var VariableCount = 0 }
+class ImmutableVariable(id: String, t: Type) extends Variable(id, t) {
+ override val IsImmutable: boolean = true
+}
+class SpecialVariable(name: String, typ: Type) extends Variable(name, typ) {
+ override val UniqueName = name
+}
+
+sealed abstract class Specification extends ASTNode
+case class Precondition(e: Expression) extends Specification
+case class Postcondition(e: Expression) extends Specification
+case class LockChange(ee: List[Expression]) extends Specification
+
+// statements
+
+sealed abstract class Statement extends ASTNode
+case class Assert(e: Expression) extends Statement
+case class Assume(e: Expression) extends Statement
+case class BlockStmt(ss: List[Statement]) extends Statement
+case class IfStmt(guard: Expression, thn: BlockStmt, els: Option[Statement]) extends Statement
+case class WhileStmt(guard: Expression,
+ invs: List[Expression], lkch: List[Expression],
+ body: BlockStmt) extends Statement {
+ var LoopTargets: Set[Variable] = null
+ lazy val LoopTargetsList: List[Variable] = { // to be called only after LoopTargets has been completely filled in
+ var vv = List[Variable]()
+ LoopTargets foreach (v => vv = v :: vv)
+ vv
+ }
+}
+case class Assign(lhs: VariableExpr, rhs: RValue) extends Statement
+case class FieldUpdate(lhs: MemberAccess, rhs: RValue) extends Statement
+case class LocalVar(id: String, t: Type, const: boolean, ghost: boolean, rhs: Option[RValue]) extends Statement {
+ val v =
+ if (const)
+ new ImmutableVariable(id, t){override val IsGhost = ghost}
+ else
+ new Variable(id, t){override val IsGhost = ghost}
+}
+case class Call(lhs: List[VariableExpr], obj: Expression, id: String, args: List[Expression]) extends Statement {
+ var m: Method = null
+}
+case class Install(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement
+case class Share(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement
+case class Unshare(obj: Expression) extends Statement
+case class Acquire(obj: Expression) extends Statement
+case class Release(obj: Expression) extends Statement
+case class RdAcquire(obj: Expression) extends Statement
+case class RdRelease(obj: Expression) extends Statement
+case class Downgrade(obj: Expression) extends Statement
+case class Lock(obj: Expression, b: BlockStmt, rdLock: boolean) extends Statement
+case class Free(obj: Expression) extends Statement
+case class CallAsync(declaresLocal: boolean, lhs: VariableExpr, obj: Expression, id: String, args: List[Expression]) extends Statement {
+ var local: Variable = null
+ var m: Method = null
+}
+case class JoinAsync(lhs: List[VariableExpr], token: Expression) extends Statement {
+ var m: Method = null
+}
+
+case class Fold(pred: PermissionExpr) extends Statement
+case class Unfold(pred: PermissionExpr) extends Statement
+
+// expressions
+
+sealed abstract class RValue extends ASTNode {
+ var typ: Class = null
+}
+case class NewRhs(id: String, initialization: List[Init]) extends RValue
+case class Init(id: String, e: Expression) extends ASTNode {
+ var f: Field = null;
+}
+sealed abstract class Expression extends RValue
+sealed abstract class Literal extends Expression
+case class IntLiteral(n: int) extends Literal
+case class BoolLiteral(b: boolean) extends Literal
+case class NullLiteral extends Literal
+case class MaxLockLiteral extends Literal
+case class LockBottomLiteral extends Literal
+case class VariableExpr(id: String) extends Expression {
+ var v: Variable = null
+ def this(vr: Variable) = { this(vr.id); v = vr; typ = vr.t.typ }
+}
+case class Result extends Expression
+sealed abstract class ThisExpr extends Expression {
+ override def equals(other: Any): Boolean = {
+ // needed in autoMagic, which checks for syntactic equality using equals
+ other.isInstanceOf[ThisExpr]
+ }
+}
+case class ExplicitThisExpr extends ThisExpr
+case class ImplicitThisExpr extends ThisExpr
+case class MemberAccess(e: Expression, id: String) extends Expression {
+ var isPredicate: Boolean = false;
+ var f: Field = null
+ var predicate: Predicate = null
+}
+case class IfThenElse(con: Expression, then: Expression, els: Expression) extends Expression
+
+sealed abstract class PermissionExpr extends Expression {
+ def getMemberAccess : MemberAccess
+}
+
+case class Access(e: MemberAccess, perm: Option[Expression]) extends PermissionExpr {
+ def getMemberAccess = e : MemberAccess;
+}
+case class RdAccess(e: MemberAccess, perm: Option[Option[Expression]]) extends PermissionExpr {
+ 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 Holds(e: Expression) extends Expression
+case class RdHolds(e: Expression) extends Expression
+case class Assigned(id: String) extends Expression {
+ var v: Variable = null
+}
+case class Old(e: Expression) extends Expression
+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
+sealed abstract class BinaryExpr(e0: Expression, e1: Expression) extends Expression {
+ def E0 = e0
+ def E1 = e1
+ def ExpectedLhsType: Class = BoolClass // sometimes undefined
+ def ExpectedRhsType: Class = BoolClass // sometimes undefined
+ val ResultType: Class = BoolClass
+ val OpName: String
+}
+case class Iff(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
+ override val OpName = "<==>"
+}
+case class Implies(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
+ override val OpName = "==>"
+}
+case class And(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
+ override val OpName = "&&"
+}
+case class Or(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
+ override val OpName = "||"
+}
+sealed abstract class ArithmeticExpr(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
+ override def ExpectedLhsType = IntClass
+ override def ExpectedRhsType = IntClass
+ override val ResultType = IntClass
+}
+case class Plus(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
+ override val OpName = "+"
+}
+case class Minus(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
+ override val OpName = "-"
+}
+case class Times(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
+ override val OpName = "*"
+}
+case class Div(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
+ override val OpName = "/"
+}
+case class Mod(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
+ override val OpName = "%"
+}
+sealed abstract class CompareExpr(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
+ override def ExpectedLhsType = IntClass
+ override def ExpectedRhsType = IntClass
+}
+sealed abstract class EqualityCompareExpr(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
+ override def ExpectedLhsType = throw new Exception("EqualityCompareExpr does not have a single ExpectedArgsType")
+ override def ExpectedRhsType = throw new Exception("EqualityCompareExpr does not have a single ExpectedArgsType")
+}
+case class Eq(e0: Expression, e1: Expression) extends EqualityCompareExpr(e0,e1) {
+ override val OpName = "=="
+}
+case class Neq(e0: Expression, e1: Expression) extends EqualityCompareExpr(e0,e1) {
+ override val OpName = "!="
+}
+case class Less(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
+ override val OpName = "<"
+}
+case class AtMost(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
+ override val OpName = "<="
+}
+case class AtLeast(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
+ override val OpName = ">="
+}
+case class Greater(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
+ override val OpName = ">"
+}
+case class LockBelow(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
+ override def ExpectedLhsType = throw new Exception("LockBelow does not have a single ExpectedArgsType")
+ override def ExpectedRhsType = throw new Exception("LockBelow does not have a single ExpectedArgsType")
+ override val OpName = "<<"
+}
+sealed abstract class Quantification(is: List[String], seq: Expression, e: Expression) extends Expression {
+ def Quantor: String;
+ def Is = is
+ def Seq = seq
+ def E = e
+ var variables = null: List[Variable];
+}
+case class Forall(is: List[String], seq: Expression, e: Expression) extends Quantification(is, seq, e) {
+ override def Quantor = "forall"
+}
+
+// sequences
+
+case class EmptySeq(t: Type) extends Literal
+case class ExplicitSeq(elems: List[Expression]) extends Expression
+case class Range(min: Expression, max: Expression /* non-inclusive*/) extends Expression
+case class Append(s0: Expression, s1: Expression) extends SeqAccess(s0, s1) {
+ override val OpName = "++"
+}
+ sealed abstract case class SeqAccess(e0: Expression, e1: Expression) extends BinaryExpr(e0, e1)
+case class Length(e: Expression) extends Expression
+case class At(s: Expression, n: Expression) extends SeqAccess(s, n) {
+ override val OpName = "@"
+}
+case class Drop(s: Expression, n: Expression) extends SeqAccess(s, n) {
+ override val OpName = ""
+}
+case class Take(s: Expression, n: Expression) extends SeqAccess(s, n) {
+ override val OpName = ""
+}
+
+
+// eval
+
+case class Eval(h: EvalState, e: Expression) extends Expression
+sealed abstract class EvalState {
+ def target(): Expression;
+}
+case class AcquireState(obj: Expression) extends EvalState {
+ def target() = obj
+}
+case class ReleaseState(obj: Expression) extends EvalState {
+ def target() = obj
+}
+case class CallState(token: Expression, obj: Expression, id: String, args: List[Expression]) extends EvalState {
+ var m = null: Method;
+ def target() = token;
+}
diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala new file mode 100644 index 00000000..492e0669 --- /dev/null +++ b/Chalice/src/Boogie.scala @@ -0,0 +1,270 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+import scala.util.parsing.input.Position
+import scala.util.parsing.input.NoPosition
+
+object Boogie {
+
+ sealed abstract class Decl
+ case class Const(id: String, unique: boolean, t: BType) extends Decl
+ case class Proc(id: String, ins: List[BVar], outs: List[BVar],
+ mod: List[String], PrePost: List[String],
+ body: List[Stmt]) extends Decl
+ case class Function(id: String, ins: List[BVar], out: BVar) extends Decl
+ case class Axiom(expr: Expr) extends Decl
+
+ sealed abstract class BType
+ case class NamedType(s: String) extends BType
+ case class ClassType(cl: Class) extends BType
+ case class IndexedType(id: String, t: BType) extends BType
+
+ sealed abstract class Stmt {
+ def Locals = List[BVar]()
+ }
+ case class Comment(comment: String) extends Stmt
+ case class Assert(e: Expr) extends Stmt {
+ def this(e: Expr, p: Position, txt: String) = { this(e); this.pos = p; this.message = txt; this }
+ var pos = NoPosition : Position
+ var message = "" : String
+ }
+ case class Assume(e: Expr) extends Stmt
+ case class Assign(lhs: Expr, rhs: Expr) extends Stmt
+ case class AssignMap(lhs: Expr, index: Expr, rhs: Expr) extends Stmt
+ case class Havoc(x: Expr) extends Stmt
+ case class MapUpdate(map: Expr, arg0: Expr, arg1: String, rhs: Expr) extends Stmt {
+ def this(map: Expr, arg0: Expr, rhs: Expr) = this(map, arg0, null, rhs)
+ }
+ case class If(guard: Expr, thn: List[Stmt], els: List[Stmt]) extends Stmt {
+ override def Locals = (thn flatMap (_.Locals)) ::: (els flatMap (_.Locals))
+ }
+ case class LocalVar(x: BVar) extends Stmt {
+ def this(id: String, tp: BType) = this(BVar(id, tp))
+
+ override def Locals = List(x)
+ }
+
+ sealed abstract class Expr {
+ def &&(that: Expr) = BinaryExpr("&&", this, that)
+ def ||(that: Expr) = BinaryExpr("||", this, that)
+ def ==@(that: Expr) = BinaryExpr("==", this, that)
+ def !=@(that: Expr) = BinaryExpr("!=", this, that)
+ def Equals(that: Expr) = BinaryExpr("==", this, that)
+ def ==>(that: Expr) = BinaryExpr("==>", this, that)
+ def <==>(that: Expr) = BinaryExpr("<==>", this, that)
+ def unary_! = UnaryExpr("!", this)
+ def <=(that: Expr) = BinaryExpr("<=", this, that)
+ def <(that: Expr) = BinaryExpr("<", this, that)
+ def >=(that: Expr) = BinaryExpr(">=", this, that)
+ def >(that: Expr) = BinaryExpr(">", this, that)
+ def +(that: Expr) = BinaryExpr("+", this, that)
+ def -(that: Expr) = BinaryExpr("-", this, that)
+ def *(that: Expr) = BinaryExpr("*", this, that)
+ def /(that: Expr) = BinaryExpr("/", this, that)
+ def %(that: Expr) = BinaryExpr("%", this, that)
+ def := (that: Expr) = Assign(this, that)
+ def select(e: Expr, f: Expr) = new MapSelect(this, e, PrintExpr(f))
+ def store(e: Expr, f: Expr, rhs: Expr) = MapUpdate(this, e, PrintExpr(f), rhs)
+ }
+ case class IntLiteral(n: int) extends Expr
+ case class BoolLiteral(b: boolean) extends Expr
+ case class Null extends Expr
+ case class VarExpr(id: String) extends Expr {
+ def this(v: BVar) = this(v.id)
+ }
+ case class MapSelect(map: Expr, arg0: Expr, arg1: String) extends Expr {
+ def this(map: Expr, arg0: Expr) = this(map, arg0, null) // for one-dimensional maps
+ def this(map: Expr, arg0: Expr, arg1: String, arg2: String) = // for 3-dimensional maps
+ this(MapSelect(map, arg0, arg1), VarExpr(arg2), null)
+ }
+ case class MapStore(map: Expr, arg0: String, rhs: Expr) extends Expr
+ case class Old(e: Expr) extends Expr
+ case class UnaryExpr(op: String, e: Expr) extends Expr
+ case class BinaryExpr(op: String, e0: Expr, e1: Expr) extends Expr
+ case class FunctionApp(f: String, args: List[Expr]) extends Expr {
+ def this(f: String, a0: Expr) = this(f, List(a0))
+ def this(f: String, a0: Expr, a1: Expr) = this(f, List(a0, a1))
+ def this(f: String, a0: Expr, a1: Expr, a2: Expr) = this(f, List(a0, a1, a2))
+ }
+ case class Forall(ta: List[TVar], xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr {
+ def this(xs: List[BVar], triggers: List[Expr], body: Expr) = this(List(), xs, triggers, body)
+ def this(x: BVar, body: Expr) = this(List(), List(x), List(), body)
+ def this(t: TVar, x: BVar, body: Expr) = this(List(t), List(x), List(), body)
+ }
+ case class Exists(xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr {
+ def this(x: BVar, body: Expr) = this(List(x), List(), body)
+ }
+ case class Ite(con: Expr, then: Expr, els: Expr) extends Expr
+
+ case class BVar(id: String, t: BType) {
+ def this(id: String, t: BType, uniquifyName: boolean) =
+ this(if (uniquifyName) {
+ val n = S_BVar.VariableCount
+ S_BVar.VariableCount = S_BVar.VariableCount + 1
+ id + "#_" + n
+ } else {
+ id
+ }, t)
+ val where: Expr = null
+ }
+ object S_BVar { var VariableCount = 0 }
+ def NewBVar(id: String, t: BType, uniquifyName: boolean) = {
+ val v = new Boogie.BVar(id, t, uniquifyName)
+ val e = new Boogie.VarExpr(v)
+ (v,e)
+ }
+ case class TVar(id: String) {
+ def this(id: String, uniquifyName: boolean) =
+ this(if (uniquifyName) {
+ val n = S_TVar.VariableCount
+ S_TVar.VariableCount = S_TVar.VariableCount + 1
+ id + "#_" + n
+ } else {
+ id
+ })
+ val where: Expr = null
+ }
+ object S_TVar { var VariableCount = 0 }
+ def NewTVar(id: String) = {
+ val v = new Boogie.TVar(id, true)
+ val e = new Boogie.NamedType(v.id)
+ (v,e)
+ }
+
+ // def out(s: String) = Console.out.print(s)
+ var indentLevel = 1
+ def indent: String = {
+ def doIndent(i: int): String = {
+ if(i==0) { "" } else { " " + doIndent(i-1) }
+ }
+ doIndent(indentLevel);
+ }
+
+ def IndentMore(what: => String) = {
+ val prev = indentLevel
+ indentLevel = indentLevel + 1
+ val result = what
+ indentLevel = prev
+ result
+ }
+ def nl = System.getProperty("line.separator");
+
+ def Print[T](list: List[T], sep: String, p: T => String): String = list match {
+ case Nil => ""
+ case x :: Nil => p(x)
+ case x :: xs => p(x) + sep + Print(xs, sep, p)
+ }
+ def PrintType(t: BType): String = t match {
+ case nt@ NamedType(s) =>
+ s
+ case ClassType(cl) =>
+ if (cl.IsRef) "ref" else cl.id
+ case IndexedType(id,t) =>
+ id + " (" + PrintType(t) + ")"
+ }
+ def Print(d: Decl): String = d match {
+ case Const(id, u, t) =>
+ "const " + (if (u) "unique " else "" ) + id + ": " + PrintType(t) + ";" + nl
+ case p: Proc =>
+ "procedure " + p.id +
+ "(" + Print(p.ins, ", ", PrintVar) + ")" +
+ " returns (" + Print(p.outs, ", ", PrintVar) + ")" + nl +
+ (p.mod match {
+ case Nil => ""
+ case x :: xs =>
+ indent + "modifies " +
+ Print(p.mod, ", ", { s: String => s }) +
+ ";" + nl
+ }) +
+ Print(p.PrePost, nl, { spec: String => indent + spec }) + nl +
+ "{" + nl +
+ Print(p.body flatMap (_.Locals), "", { v:BVar => indent + "var " + PrintVar(v) + ";" + nl}) +
+ Print(p.body, "", PrintStmt) +
+ "}" + nl
+ case Function(id, ins, out) =>
+ "function " + id + "(" + Print(ins, ", ", PrintVar) + ") returns (" + PrintVar(out) + ");" + nl
+ case Axiom(e) =>
+ "axiom " + PrintExpr(e) + ";" + nl
+ }
+ def PrintVar(v: BVar): String = {
+ v.id + ": " + PrintType(v.t) +
+ (if (v.where != null) {" where " + PrintExpr(v.where) } else { "" })
+ }
+ def PrintStmt(s: Stmt): String = s match {
+ case Comment(msg) => indent + "// " + msg + nl
+ case assert@Assert(e) => indent + "assert " + "{:msg \" " + assert.pos + ": " + assert.message + "\"}" + " " + PrintExpr(e) + ";" + nl
+ case Assume(e) => indent + "assume " + PrintExpr(e) + ";" + nl
+ case If(guard, thn, els) =>
+ indent + "if (" +
+ (if (guard == null) "*" else PrintExpr(guard)) +
+ ") {" + nl +
+ IndentMore { Print(thn, "", PrintStmt) } +
+ indent + "} else {" + nl +
+ IndentMore { Print(els, "", PrintStmt) } +
+ indent + "}" + nl
+ case Assign(lhs, rhs) =>
+ indent + PrintExpr(lhs) + " := " + PrintExpr(rhs) + ";" + nl
+ case AssignMap(lhs, index, rhs) =>
+ indent + PrintExpr(lhs) + "[" + PrintExpr(index) + "] := " + PrintExpr(rhs) + ";" + nl
+ case Havoc(lhs) =>
+ indent + "havoc " + PrintExpr(lhs) + ";" + nl
+ case MapUpdate(map, a0, a1, rhs) =>
+ indent + PrintExpr(map) + "[" +
+ PrintExpr(a0) +
+ (if (a1 != null) { ", " + a1 } else { "" }) +
+ "] := " +
+ PrintExpr(rhs) + ";" + nl
+ case _:LocalVar => "" /* print nothing */
+ }
+ def PrintExpr(e: Expr): String = {
+ PrintExpr(e, false)
+ }
+ def PrintExpr(e: Expr, useParens: boolean): String = e match {
+ case IntLiteral(n) => n.toString
+ case BoolLiteral(b) => b.toString
+ case Null() => "null"
+ case VarExpr(id) => id
+ case MapSelect(map, arg0, arg1) =>
+ PrintExpr(map) + "[" + PrintExpr(arg0, false) +
+ (if (arg1 != null) { ", " + arg1 } else { "" }) +
+ "]"
+ case MapStore(map, arg0, rhs) =>
+ PrintExpr(map) + "[" + arg0 + " := " + PrintExpr(rhs, false) + "]"
+ case Old(e) => "old(" + PrintExpr(e, false) + ")"
+ case UnaryExpr(op, e) =>
+ (if (useParens) { "(" } else "") +
+ op + PrintExpr(e, true) +
+ (if (useParens) ")" else "" )
+ case BinaryExpr(op, e0, e1) =>
+ // reduce parentheses in a special common case:
+ val binIsAndImpIff = op=="&&" || op=="==>" || op=="<==>";
+ def IsAnd(e: Expr) = e match { case BinaryExpr(op,_,_) if op=="&&" => true case _ => false }
+ (if (useParens) "(" else "") + PrintExpr(e0, !(binIsAndImpIff && IsAnd(e0))) +
+ " " + op + " " +
+ PrintExpr(e1, !(binIsAndImpIff && IsAnd(e1))) +
+ (if (useParens) ")" else "")
+ case FunctionApp(f, args) =>
+ f + "(" +
+ Print(args, ", ", { e: Expr => PrintExpr(e, false) }) +
+ ")"
+ case Ite(con, then, els) =>
+ "ite(" + PrintExpr(con) + ", " + PrintExpr(then) + ", " + PrintExpr(els) + ")"
+ case Forall(ts, xs, triggers, body) =>
+ "(forall" +
+ (if (ts.length == 0) " " else "<" + Print(ts, ", ", { x: TVar => x.id }) + "> ") +
+ Print(xs, ", ", { x: BVar => x.id + ": " + PrintType(x.t) }) +
+ " :: " +
+ Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) +
+ PrintExpr(body) +
+ ")"
+ case Exists(xs, triggers, body) =>
+ "(exists " +
+ Print(xs, ", ", { x: BVar => x.id + ": " + PrintType(x.t) }) +
+ " :: " +
+ Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) +
+ PrintExpr(body) +
+ ")"
+ }
+}
diff --git a/Chalice/src/Chalice.cs b/Chalice/src/Chalice.cs new file mode 100644 index 00000000..f4a804e7 --- /dev/null +++ b/Chalice/src/Chalice.cs @@ -0,0 +1,76 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System.Collections.Generic;
+using System.Linq;
+
+namespace Chalice
+{
+ public class ImmutableList<E>
+ {
+ private List<E> list;
+
+ public ImmutableList() {
+ list = new List<E>();
+ }
+
+ public ImmutableList(IEnumerable<E> elems)
+ {
+ list = new List<E>(elems);
+ }
+
+ public ImmutableList<E> Append(ImmutableList<E> other)
+ {
+ var res = new ImmutableList<E>();
+ res.list.AddRange(list);
+ res.list.AddRange(other.list);
+ return res;
+ }
+
+ public E At(int index)
+ {
+ return list[index];
+ }
+
+ public ImmutableList<E> Take(int howMany)
+ {
+ var res = new ImmutableList<E>(this.list.Take(howMany));
+ return res;
+ }
+
+ public ImmutableList<E> Drop(int howMany)
+ {
+ var res = new ImmutableList<E>(this.list.Skip(howMany));
+ return res;
+ }
+
+ public int Length
+ {
+ get
+ {
+ return list.Count;
+ }
+ }
+
+ public static ImmutableList<int> Range(int min, int max)
+ {
+ ImmutableList<int> l = new ImmutableList<int>();
+ for (int i = min; i < max; i++)
+ {
+ l.list.Add(i);
+ }
+ return l;
+ }
+ }
+
+ public class ChalicePrint {
+ public void Int(int x) {
+ System.Console.WriteLine(x);
+ }
+ public void Bool(bool x) {
+ System.Console.WriteLine(x);
+ }
+ }
+}
diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala new file mode 100644 index 00000000..439805d4 --- /dev/null +++ b/Chalice/src/Chalice.scala @@ -0,0 +1,115 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+import java.io.BufferedReader
+import java.io.InputStreamReader
+import java.io.File
+import java.io.FileWriter
+
+object Chalice {
+ def main(args: Array[String]): unit = {
+ var boogiePath = "C:\\Boogie\\2\\Binaries\\Boogie.exe"
+ // parse command-line arguments
+ var inputName: String = null
+ var printProgram = false
+ var doTypecheck = true
+ var doTranslate = true
+ var checkLeaks = false
+ // level 0 or below: no defaults
+ // level 1: unfold predicates with receiver this in pre and postconditions
+ // level 2: unfold predicates and functions with receiver this in pre and postconditions
+ // level 3 or above: level 2 + autoMagic
+ var defaults = 0
+ var autoFold = false
+ var autoMagic = false
+ var boogieArgs = " ";
+ var gen = false;
+
+ for (a <- args) {
+ if (a == "-print") printProgram = true
+ else if (a == "-noTranslate") doTranslate = false
+ else if (a == "-noTypecheck") doTypecheck = false
+ else if (a == "-checkLeaks") checkLeaks = true
+ else if (a.startsWith("-boogie:")) boogiePath = a.substring(8)
+ else if (a == "-defaults") defaults = 3
+ else if (a.startsWith("-defaults:")) { try { defaults = Integer.parseInt(a.substring(10)); if(3<=defaults) { autoMagic = true; } } catch { case _ => CommandLineError("-defaults takes integer argument"); } }
+ else if (a == "-gen") { gen = true; doTranslate = false }
+ else if (a == "-autoFold") autoFold = true
+ else if (a == "-autoMagic") autoMagic = true
+ else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // arguments starting with "-" or "/" are sent to Boogie.exe
+ else if (inputName != null) { CommandLineError("multiple input filenames: " + inputName + " and " + a); return }
+ else { inputName = a }
+ }
+ // check the command-line arguments
+ if (inputName == null) { CommandLineError("missing input filename"); return } else {
+ val file = new File(inputName);
+ if(! file.exists()){
+ CommandLineError("input file " + file.getName() + " could not be found"); return
+ }
+ }
+ // parse program
+ val parser = new Parser();
+ parser.parseFile(inputName) match {
+ case e: parser.NoSuccess => Console.err.println("Error: " + e)
+ case parser.Success(prog, _) =>
+ if (printProgram) PrintProgram.P(prog)
+ if (doTypecheck) {
+ // typecheck program
+ Resolver.Resolve(prog) match {
+ case Resolver.Error(pos, msg) =>
+ Console.err.println("The program did not typecheck.\n");
+ Console.err.println(msg)
+ case Resolver.Errors(msgs) =>
+ Console.err.println("The program did not typecheck.");
+ msgs foreach { msg => Console.err.println(msg) }
+ case Resolver.Success() =>
+ if(gen) {
+ val converter = new ChaliceToCSharp();
+ val cs = converter.convertProgram(prog);
+ writeFile("out.cs", cs);
+ }
+ if (doTranslate) {
+ // checking if Boogie.exe exists
+ val boogieFile = new File(boogiePath);
+ if(! boogieFile.exists() || ! boogieFile.isFile()) {
+ CommandLineError("Boogie.exe not found at " + boogiePath); return
+ }
+ // translate program to BoogiePL
+ val translator = new Translator();
+ // set the translation options
+ TranslationOptions.checkLeaks = checkLeaks;
+ TranslationOptions.defaults = defaults;
+ TranslationOptions.autoFold = autoFold;
+ TranslationOptions.autoMagic = autoMagic;
+ val bplProg = translator.translateProgram(prog);
+ // write to out.bpl
+ val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b };
+ writeFile("out.bpl", bplText);
+ // run Boogie.exe on out.bpl
+ val boogie = Runtime.getRuntime().exec(boogiePath + " /errorTrace:0 " + boogieArgs + "out.bpl");
+ val input = new BufferedReader(new InputStreamReader(boogie.getInputStream()));
+ var line = input.readLine();
+ while(line!=null){
+ println(line);
+ line = input.readLine();
+ }
+ }
+ }
+ }
+ }
+ }
+
+ def writeFile(filename: String, text: String) {
+ val writer = new FileWriter(new File(filename));
+ writer.write(text);
+ writer.flush();
+ writer.close();
+ }
+
+ def CommandLineError(msg: String) = {
+ Console.err.println("Error: " + msg)
+ Console.err.println("syntax: chalice [-print] [-noTypecheck] [-noTranslate] [-boogie:path] [-defaults] [-autoFold] [-checkLeaks] inputFile")
+ }
+}
diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala new file mode 100644 index 00000000..75135e38 --- /dev/null +++ b/Chalice/src/ChaliceToCSharp.scala @@ -0,0 +1,211 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+class ChaliceToCSharp {
+
+ def convertProgram(classes: List[Class]): String = {
+ "using Chalice;" + nl + nl +
+ rep(classes map convertClass)
+ }
+
+ def convertClass(cl: Class): String = if (cl.IsExternal) "" else {
+ "public class " + cl.id + " {" + nl +
+ indentMore { indent + "public " + cl.id + "() " + "{" + nl + indent + "}" } + nl + nl +
+ (if(0 < cl.Fields.length) {
+ indentMore { indent + "public " + cl.id + "(" + repsep(cl.Fields map { f => convertType(f.typ) + " " + f.Id }, ", ") + ") " + "{" + nl +
+ indentMore { rep(cl.Fields map { f => indent + "this." + f.Id + " = " + f.Id + ";" + nl}) } +
+ indent + "}" } + nl + nl
+ } else "") +
+ indentMore { repsep(cl.members map convertMember, nl) } +
+ "}" + nl + nl
+ }
+
+ def convertMember(member: Member): String = {
+ member match {
+ case Field(id, tp) =>
+ indent + "public " + convertType(tp) + " " + id + ";" + nl
+ case meth@Method(id, ins, outs, spec, body) =>
+ var csharpmain = if(id.equals("Start") && ins.length == 0 && outs.length == 0) {
+ indent + "public static void Main() { " + nl +
+ indentMore {
+ indent + meth.Parent.id + " newObject = new " + meth.Parent.id + "();" + nl +
+ indent + "newObject.Start();" + nl
+ } +
+ indent + "}" + nl + nl
+ } else { "" };
+ var params = repsep(ins map { variable => convertType(variable.t) + " " + variable.id }, ", ") + (if(ins.length > 0 && outs.length > 0) ", " else "") +
+ repsep(outs map { variable => "out " + convertType(variable.t) + " " + variable.id }, ", ");
+ csharpmain +
+ indent + "public " + "void " + id + "(" + params + ") " + "{" + nl +
+ indentMore {
+ rep(outs map { x => indent + x.id + " = " + defaultValue(x.t) + ";" + nl } ) +
+ rep(body map convertStatement)
+ } +
+ indent + "}" + nl + nl +
+ indent + "public delegate " + "void " + id + "_delegate" + "(" + params + ");" + nl + nl +
+ indent + "public class " + "Token_" + id + " { " + nl +
+ (indentMore {
+ indent + "public " + id + "_delegate " + "del;" + nl +
+ indent + "public " + "System.IAsyncResult " + "async;" + nl +
+ (rep(outs map { o: Variable => indent + "public " + convertType(o.t) + " " + o.id + ";" + nl }))
+ }) +
+ indent + "}" + nl
+ case Function(id, ins, out, spec, definition) =>
+ indent + "public " + convertType(out) + " " + id + "(" +
+ repsep(ins map { variable => convertType(variable.t) + " " + variable.id }, ", ") +
+ ") " + "{" + nl +
+ indentMore { indent + "return " + convertExpression(definition) + ";" + nl } +
+ indent + "}" + nl
+ case MonitorInvariant(_) => indent + "// monitor invariant" + nl
+ case Predicate(_, _) => indent + "//predicate" + nl
+ }
+ }
+
+ def convertStatement(statement: Statement): String = {
+ statement match {
+ case Assert(e) => indent + "// assert" + nl
+ case Assume(e) => indent + "assert " + convertExpression(e) + ";" // todo: what if e contains old, result, ...
+ case BlockStmt(ss) => indent + "{" + nl + (indentMore { rep(ss map convertStatement) }) + indent + "}" + nl
+ case IfStmt(guard, thn, els) => indent + "if (" + convertExpression(guard) + ")" + nl + convertStatement(thn) +
+ (if(els.isDefined) (indent + "else" + nl + convertStatement(els.get)) else { "" }) + nl
+ case LocalVar(id, tp, const, ghost, rhs) =>
+ indent + convertType(tp) + " " + id + " = " +
+ (if(rhs.isDefined) convertExpression(rhs.get) else defaultValue(tp)) +
+ ";" + nl
+ case FieldUpdate(MemberAccess(target, f), rhs) =>
+ indent + convertExpression(target) + "." + f + " = " + convertExpression(rhs) + ";" + nl
+ case Assign(VariableExpr(x), rhs) =>
+ indent + x + " = " + convertExpression(rhs) + ";" + nl
+ case WhileStmt(guard, _, _, body) =>
+ indent + "while (" + convertExpression(guard) + ")" + nl + convertStatement(body) + nl
+ case Call(lhs, target, id, args) =>
+ indent + convertExpression(target) + "." + id + "(" +
+ repsep(args map convertExpression, ", ") +
+ (if(args.length > 0 && lhs.length > 0) ", " else "") +
+ repsep(lhs map { l => "out " + convertExpression(l) }, ", ") +
+ ")" + ";" + nl
+ case Install(_, _, _) => indent + "// install" + nl
+ case Share(_, _, _) => indent + "// share" + nl
+ case Unshare(_) => indent + "// unshare" + nl
+ case Downgrade(_) => indent + "// downgrade" + nl
+ case Acquire(obj) => indent + "System.Threading.Monitor.Enter(" + convertExpression(obj) + ")" + ";" + nl
+ case Release(obj) => indent + "System.Threading.Monitor.Exit(" + convertExpression(obj) + ")" + ";" + nl
+ case Lock(obj, body, false) => indent + "lock(" + convertExpression(obj) + ") " + nl + convertStatement(body) + nl
+ case Free(_) => indent + "// free" + nl
+ case Fold(_) => indent + "// fold" + nl
+ case Unfold(_) => indent + "// unfold" + nl
+ case RdAcquire(obj) => assert(false); ""
+ case RdRelease(obj) => assert(false); ""
+ case Lock(_, _, true) => assert(false); ""
+ case ca@CallAsync(declaresLocal, lhs, obj, id, args) =>
+ val tokenName = if(declaresLocal) lhs.id else { uniqueInt += 1; "tok_" + uniqueInt };
+ val call = convertExpression(obj) + "." + id;
+ val tokenClass = ca.m.Parent.id + ".Token_" + id;
+ val delegateName = ca.m.Parent.id + "." + id + "_delegate";
+ indent + tokenClass + " " + tokenName + " = new " + tokenClass + "();" + nl +
+ indent + tokenName + "." + "del" + " = new " + delegateName + "(" + call + ");" + nl +
+ indent + tokenName + "." + "async" + " = " + tokenName + "." + "del" + "." + "BeginInvoke(" + repsep(args map convertExpression, ", ") +
+ (if(args.length > 0 && ca.m.outs.length > 0) ", " else "") + repsep(ca.m.outs map { o => "out " + tokenName + "." + o.id }, ", ") +
+ (if(args.length > 0 || ca.m.outs.length > 0) ", " else "") + "null, null" +
+ ");" + nl
+ case ja@JoinAsync(lhs, token) =>
+ indent + convertExpression(token) + "." + "del.EndInvoke(" +
+ repsep(lhs map { x => "out " + x.id}, ", ") +
+ (if(lhs.length > 0) ", " else "") + convertExpression(token) + "." + "async" + ");" + nl
+ }
+ }
+
+ def convertExpression(expression: RValue): String = {
+ expression match {
+ case IntLiteral(n) => "" + n
+ case BoolLiteral(b) => "" + b
+ case NullLiteral() => "null"
+ case th: ThisExpr => "this"
+ case VariableExpr(id) => id
+ case MemberAccess(target, f) => convertExpression(target) + "." + f
+ case newrhs@NewRhs(c, initialization) =>
+ if(initialization.length == 0) { "new " + c + "()" } else {
+ val init = repsep(newrhs.typ.Fields map { f => (initialization.find { i => i.f == f}) match {
+ case None => defaultValue(f.typ)
+ case Some(init) => convertExpression(init.e);
+ }
+ }, ", ");
+ "new " + c + "(" + init + ")";
+ }
+ case At(s, i) => convertExpression(s) + ".At(" + convertExpression(i) + ")"
+ case Append(s1, s2) => convertExpression(s1) + ".Append(" + convertExpression(s2) + ")"
+ case Take(s, i) => convertExpression(s) + ".Take(" + convertExpression(i) + ")"
+ case Drop(s, i) => convertExpression(s) + ".Drop(" + convertExpression(i) + ")"
+ case bin: BinaryExpr => "(" + convertExpression(bin.E0) + " " + bin.OpName + " " + convertExpression(bin.E1) + ")"// todo: <==> and ==>
+ case Unfolding(p, e) => convertExpression(e)
+ case FunctionApplication(target, id, args) => convertExpression(target) + "." + id + "(" + repsep(args map convertExpression, ", ") + ")"
+ case Not(e) => "(! " + convertExpression(e) + ")"
+ case EmptySeq(tp) => "new Chalice.ImmutableList<" + convertType(tp) + ">()"
+ case es@ExplicitSeq(elems) =>
+ val elemType = new Type(es.typ.asInstanceOf[SeqClass].parameter);
+ "new Chalice.ImmutableList<" + convertType(elemType) + ">(" +
+ "new " + convertType(elemType) + "[] {" + repsep(elems map convertExpression, ", ") + "}" +
+ ")"
+ 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) + ")"
+ }
+ }
+
+ def convertType(tp: Type): String = {
+ tp.typ match {
+ case t: TokenClass => t.c.FullName + ".Token_" + t.m
+ case s: SeqClass => "Chalice.ImmutableList<" + convertType(new Type(s.parameter)) + ">"
+ case IntClass => "int"
+ case BoolClass => "bool"
+ case NullClass => "object"
+ case Class(id, _, _, _) => id
+ }
+ }
+
+ def defaultValue(tp: Type) = {
+ tp.typ match {
+ case t: TokenClass => "null"
+ case s: SeqClass => "new Chalice.ImmutableList<" + convertType(new Type(s.parameter)) + ">()"
+ case IntClass => "0"
+ case BoolClass => "false"
+ case NullClass => "null"
+ case Class(id, _, _, _) => "null"
+ }
+ }
+
+ // utility methods below
+
+ var uniqueInt: int = 0;
+ val nl = System.getProperty("line.separator");
+ var indentLevel = 0
+
+ def rep(strings: List[String]): String = {
+ strings.foldLeft("")({ (a, b) => a + b })
+ }
+
+ def repsep(strings: List[String], separator: String): String = {
+ if(strings.length == 0) {
+ ""
+ } else {
+ strings.reduceLeft({ (a, b) => a + separator + b })
+ }
+ }
+
+ def indent: String = {
+ def doIndent(i: int): String = {
+ if(i==0) { "" } else { " " + doIndent(i-1) }
+ }
+ doIndent(indentLevel);
+ }
+
+ def indentMore(what: => String) = {
+ val prev = indentLevel
+ indentLevel = indentLevel + 1
+ val result = what
+ indentLevel = prev
+ result
+ }
+}
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala new file mode 100644 index 00000000..5063cc92 --- /dev/null +++ b/Chalice/src/Parser.scala @@ -0,0 +1,409 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+import scala.util.parsing.combinator.syntactical.StandardTokenParsers
+import scala.util.parsing.input.PagedSeqReader
+import scala.collection.immutable.PagedSeq
+import scala.util.parsing.input.Position
+import scala.util.parsing.input.Positional
+import scala.util.parsing.input.NoPosition
+
+class Parser extends StandardTokenParsers {
+
+ def parseFile(path: String): this.ParseResult[List[Class]] = {
+ val tokens = new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile path));
+ phrase(programUnit)(tokens)
+ }
+
+ case class PositionedString(v: String) extends Positional
+
+ lexical.reserved += ("class", "ghost", "var", "const", "method", "assert", "assume", "new", "this", "reorder",
+ "between", "and", "above", "below", "share", "unshare", "acquire", "release", "downgrade",
+ "lock", "fork", "join", "rd", "acc", "holds", "old", "assigned",
+ "call", "if", "else", "while", "invariant", "lockchange",
+ "returns", "requires", "ensures", "int", "bool", "false", "true", "null", "maxlock", "lockbottom",
+ "module", "external",
+ "predicate", "function", "free", "ite", "fold", "unfold", "unfolding", "in", "forall", "exists",
+ "seq", "nil", "result", "eval", "token")
+ // todo: can we remove "nil"?
+ lexical.delimiters += ("(", ")", "{", "}",
+ "<==>", "==>", "&&", "||",
+ "==", "!=", "<", "<=", ">=", ">", "<<",
+ "+", "-", "*", "/", "%", "!", ".", "..",
+ ";", ":", ":=", ",", "?", "|", "@", "[", "]", "++")
+
+ def programUnit = classDecl*
+
+ // class and members
+
+ def classDecl =
+ positioned(("external" ?) ~ ("class" ~> ident) ~ opt("module" ~> ident) ~ "{" ~ (memberDecl*) <~ "}" ^^ {
+ case ext ~ id ~ module ~ _ ~ members =>
+ val cl = Class(id, Nil, module.getOrElse("default"), members)
+ ext match { case None => case Some(t) => cl.IsExternal = true }
+ cl
+ })
+ def memberDecl = positioned(fieldDecl | invariantDecl | methodDecl | predicateDecl | functionDecl)
+
+ def fieldDecl =
+ ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id,t) }
+ | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => new Field(id,t){override val IsGhost = true} }
+ )
+ def Ident =
+ positioned(ident ^^ PositionedString)
+ def idType =
+ idTypeOpt ^^ {
+ case (id, None) => (id, Type("int", Nil))
+ case (id, Some(t)) => (id, t) }
+ def idTypeOpt =
+ ident ~ (":" ~> typeDecl ?) ^^ { case id ~ optT => (id, optT) }
+ def typeDecl: Parser[Type] =
+ positioned(("int" | "bool" | ident | "seq") ~ opt("<" ~> repsep(typeDecl, ",") <~ ">") ^^ { case t ~ parameters => Type(t, parameters.getOrElse(Nil)) }
+ | ("token" ~ "<") ~> (typeDecl <~ ".") ~ ident <~ ">" ^^ { case c ~ m => TokenType(c, m) }
+ )
+ def Semi = ";" ?
+
+ def invariantDecl = positioned("invariant" ~> expression <~ Semi ^^ MonitorInvariant)
+
+ def methodDecl =
+ "method" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~
+ (methodSpec*) ~ blockStatement ^^ {
+ case id ~ ins ~ outs ~ spec ~ body =>
+ currentLocalVariables = Set[String]()
+ outs match {
+ case None => Method(id, ins, Nil, spec, body)
+ case Some(outs) => Method(id, ins, outs, spec, body) }}
+ def predicateDecl: Parser[Predicate] =
+ ("predicate" ~> ident) ~ ("{" ~> expression <~ "}") ^^ { case id ~ definition => Predicate(id, definition) }
+ def functionDecl =
+ ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ ("{" ~> expression <~ "}") ^^ { case id ~ ins ~ out ~ specs ~ body => Function(id, ins, out, specs, body) }
+ def formalParameters(immutable: boolean) =
+ "(" ~> (formalList(immutable) ?) <~ ")" ^^ {
+ 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 }
+ }
+ def methodSpec =
+ positioned( "requires" ~> expression <~ Semi ^^ Precondition
+ | "ensures" ~> expression <~ Semi ^^ Postcondition
+ | "lockchange" ~> expressionList <~ Semi ^^ LockChange
+ )
+ def blockStatement: Parser[List[Statement]] = {
+ val prev = currentLocalVariables
+ "{" ~> (statement*) <~ "}" ^^ {
+ case x => currentLocalVariables = prev; x }
+ }
+
+ // statements
+
+ def statement =
+ positioned( "assert" ~> expression <~ Semi ^^ Assert
+ | "assume" ~> expression <~ Semi ^^ Assume
+ | blockStatement ^^ BlockStmt
+ | "var" ~> localVarStmt(false, false)
+ | "const" ~> localVarStmt(true, false)
+ | "ghost" ~> ( "const" ~> localVarStmt(true, true) | "var" ~> localVarStmt(false, true))
+ | "call" ~> callStmt
+ | "if" ~> ifStmtThen
+ | "while" ~> "(" ~> expression ~ ")" ~ loopSpec ~ blockStatement ^^ {
+ case guard ~ _ ~ lSpec ~ body =>
+ lSpec match { case (invs,lkch) => WhileStmt(guard, invs, lkch, BlockStmt(body)) }}
+ | "reorder" ~> expression ~ (installBounds ?) <~ Semi ^^ {
+ case obj ~ None => Install(obj, List(), List())
+ case obj ~ Some(bounds) => Install(obj, bounds._1, bounds._2) }
+ | "share" ~> expression ~ (installBounds ?) <~ Semi ^^ {
+ case obj ~ None => Share(obj, List(), List())
+ case obj ~ Some(bounds) => Share(obj, bounds._1, bounds._2) }
+ | "unshare" ~> expression <~ Semi ^^ Unshare
+ | "acquire" ~> expression <~ Semi ^^ Acquire
+ | "release" ~> expression <~ Semi ^^ Release
+ | "lock" ~> "(" ~> expression ~ ")" ~ blockStatement ^^ {
+ case e ~ _ ~ b => Lock(e, BlockStmt(b), false) }
+ | "rd" ~>
+ ( "lock" ~> "(" ~> expression ~ ")" ~ blockStatement ^^ {
+ case e ~ _ ~ b => Lock(e, BlockStmt(b), true) }
+ | "acquire" ~> expression <~ Semi ^^ RdAcquire
+ | "release" ~> expression <~ Semi ^^ RdRelease
+ )
+ | "downgrade" ~> expression <~ Semi ^^ Downgrade
+ | "free" ~> expression <~ Semi ^^ Free
+ | Ident ~ ":=" ~ Rhs <~ Semi ^^ {
+ case lhs ~ _ ~ rhs =>
+ if (currentLocalVariables contains lhs.v) {
+ val varExpr = VariableExpr(lhs.v); varExpr.pos = lhs.pos;
+ Assign(varExpr, rhs)
+ } else {
+ val implicitThis = ImplicitThisExpr();
+ val select = MemberAccess(implicitThis, lhs.v);
+ implicitThis.pos = lhs.pos;
+ select.pos = lhs.pos;
+ FieldUpdate(select, rhs)
+ }}
+ | selectExprFerSure ~ ":=" ~ Rhs <~ Semi ^^ {
+ case lhs ~ _ ~ rhs => FieldUpdate(lhs, rhs) }
+ | ("fold" ~> expression <~ Semi) ^? {
+ case pred: MemberAccess => Fold(Access(pred, None))
+ case perm: PermissionExpr => Fold(perm)
+ }
+ | ("unfold" ~> expression <~ Semi) ^? {
+ case pred: MemberAccess => Unfold(Access(pred, None))
+ case perm: PermissionExpr => Unfold(perm)
+ }
+ | ("fork") ~> callSignature ^? ({
+ case None ~ target ~ args =>
+ val (receiver, name) = target match {
+ case VariableExpr(id) => (new ImplicitThisExpr, id)
+ case MemberAccess(obj, id) => (obj, id)
+ }
+ CallAsync(false, null, receiver, name, ExtractList(args))
+ case Some(List(tok)) ~ target ~ args =>
+ val (receiver, name) = target match {
+ case VariableExpr(id) => (new ImplicitThisExpr, id)
+ case MemberAccess(obj, id) => (obj, id)
+ }
+ if (currentLocalVariables contains tok.id) {
+ CallAsync(false, tok, receiver, name, ExtractList(args))
+ } else {
+ currentLocalVariables = currentLocalVariables + tok.id;
+ CallAsync(true, tok, receiver, name, ExtractList(args))
+ }
+ }, t => "fork statement cannot take more than 1 left-hand side")
+ | (("join") ~> ( identList <~ ":=" ?)) ~ expression <~ Semi ^^
+ { case results ~ token => JoinAsync(ExtractList(results), token) }
+ )
+ def localVarStmt(const: boolean, ghost: boolean) =
+ idTypeOpt ~ (":=" ~> Rhs ?) <~ Semi ^^ {
+ case (id,optT) ~ rhs =>
+ currentLocalVariables = currentLocalVariables + id
+ LocalVar(id,
+ optT match {
+ case Some(t) => t
+ case None =>
+ // do a cheap (and hokey) type inference of the RHS
+ rhs match {
+ case Some(NewRhs(tid, _)) => Type(tid, Nil)
+ case Some(BoolLiteral(b)) => Type("bool", Nil)
+ case _ => Type("int", Nil)
+ }
+ },
+ const, ghost, rhs)
+ }
+ def ifStmtThen: Parser[IfStmt] =
+ "(" ~> expression ~ ")" ~ blockStatement ~ ("else" ~> ifStmtElse ?) ^^ {
+ case guard ~ _ ~ thenClause ~ elseClause => IfStmt(guard, BlockStmt(thenClause), elseClause) }
+ def ifStmtElse =
+ ( "if" ~> ifStmtThen
+ | statement
+ )
+ def loopSpec: Parser[(List[Expression], List[Expression])] =
+ (loopSpecX *) ^^ {
+ case pp => (pp :\ (List[Expression](), List[Expression]())) ( (p,list) =>
+ (p,list) match {
+ case ((null,ee),(e0,e1)) => (e0, ee ++ e1)
+ case ((e,ee),(e0,e1)) => (e :: e0, ee ++ e1)
+ })
+ }
+ def loopSpecX =
+ ( "invariant" ~> expression <~ Semi ^^ { case e => (e,Nil) }
+ | "lockchange" ~> expressionList <~ Semi ^^ { case ee => (null,ee) }
+ )
+ def callStmt =
+ callSignature ^? ({
+ case outs ~ VariableExpr(id) ~ args => Call(ExtractList(outs), new ImplicitThisExpr, id, ExtractList(args))
+ case outs ~ MemberAccess(obj,id) ~ args => Call(ExtractList(outs), obj, id, ExtractList(args))
+ }, t => "bad call statement")
+ def callSignature =
+ (identList <~ ":=" ?) ~ callTarget ~ (expressionList?) <~ ")" <~ Semi
+ def callTarget = // returns a VariableExpr or a FieldSelect
+ ( ident <~ "(" ^^ VariableExpr
+ | selectExprFerSure <~ "("
+ )
+ def ExtractList[T](a: Option[List[T]]): List[T] = a match {
+ case None => Nil
+ case Some(list) => list }
+ def identList =
+ ( Ident ^^ { case t => val v = VariableExpr(t.v); v.pos = t.pos; v }) ~
+ (("," ~> Ident ^^ { case t => val v = VariableExpr(t.v); v.pos = t.pos; v }) *) ^^ { case e ~ ee => e::ee }
+ def Rhs : Parser[RValue] =
+ positioned( "new" ~> ident ~ opt("{" ~> repsep(FieldInit, ",") <~ "}") ^^ { case id ~ None => NewRhs(id, Nil)
+ case id ~ Some(inits) => NewRhs(id, inits)
+ }
+ | expression
+ )
+ def FieldInit: Parser[Init] =
+ positioned( (ident <~ ":=") ~ expression ^^ { case id ~ e => Init(id, e) } )
+ def installBounds: Parser[(List[Expression], List[Expression])] =
+ ( "between" ~> expressionList ~ "and" ~ expressionList ^^ { case l ~ _ ~ u => (l,u) }
+ | "below" ~> expressionList ^^ { (Nil,_) }
+ | "above" ~> expressionList ^^ { (_,Nil) }
+ )
+
+ // expressions
+
+ def expression = positioned(iteExpr)
+
+ def iteExpr: Parser[Expression] =
+ positioned(iffExpr ~ (("?" ~> iteExpr) ~ (":" ~> iteExpr) ?) ^^ {
+ case e ~ None => e
+ case e0 ~ Some(e1 ~ e2) => IfThenElse(e0,e1,e2) })
+ def iffExpr: Parser[Expression] =
+ positioned(implExpr ~ ("<==>" ~> iffExpr ?) ^^ {
+ case e ~ None => e
+ case e0 ~ Some(e1) => Iff(e0,e1) })
+ def implExpr: Parser[Expression] =
+ positioned(logicalExpr ~ ("==>" ~> implExpr ?) ^^ {
+ case e ~ None => e
+ case e0 ~ Some(e1) => Implies(e0,e1) })
+ def logicalExpr =
+ positioned(cmpExpr ~ (( ("&&" ~ cmpExpr +) | ("||" ~ cmpExpr +) )?) ^^ {
+ case e ~ None => e
+ case e0 ~ Some(rest) => (rest foldLeft e0) {
+ case (a, "&&" ~ b) => And(a,b)
+ case (a, "||" ~ b) => Or(a,b) }})
+ def cmpExpr =
+ positioned(seqExpr ~ ((CompareOp ~ seqExpr)?) ^^ {
+ case e ~ None => e
+ case e0 ~ Some("==" ~ e1) => Eq(e0,e1)
+ case e0 ~ Some("!=" ~ e1) => Neq(e0,e1)
+ case e0 ~ Some("<" ~ e1) => Less(e0,e1)
+ case e0 ~ Some("<=" ~ e1) => AtMost(e0,e1)
+ case e0 ~ Some(">=" ~ e1) => AtLeast(e0,e1)
+ case e0 ~ Some(">" ~ e1) => Greater(e0,e1)
+ case e0 ~ Some("<<" ~ e1) => LockBelow(e0,e1)
+ })
+ def CompareOp = "==" | "!=" | "<" | "<=" | ">=" | ">" | "<<"
+ def seqExpr =
+ positioned(addExpr ~ (seqAccess *) ^^ { case e ~ as => as.foldLeft(e: Expression)({ (t, a) => val result = a(t); result.pos = t.pos; result }) })
+
+ def seqAccess : Parser[(Expression => SeqAccess)] =
+ ( ("[" ~> expression) <~ "]" ^^ { case e1 => { e0: Expression => At(e0, e1) }}
+ | "[" ~> expression <~ (".." ~ "]") ^^ { case e1 => { e0: Expression => Drop(e0, e1)}}
+ | ("[" ~ "..") ~> expression <~ "]" ^^ { case e1 => { e0: Expression => Take(e0, e1)}}
+ | "++" ~> expression ^^ { case e1 => { e0: Expression => Append(e0, e1) }}
+ | ("[" ~> expression <~ "..") ~ (expression <~ "]") ^^ { case e1 ~ e2 => {e0: Expression => val tak = Take(e0, e2); tak.pos = e0.pos; Drop(tak, e1)} })
+
+ def addExpr =
+ positioned(multExpr ~ (AddOp ~ multExpr *) ^^ {
+ case e0 ~ rest => (rest foldLeft e0) {
+ case (a, "+" ~ b) => Plus(a,b)
+ case (a, "-" ~ b) => Minus(a,b) }})
+ def AddOp = "+" | "-"
+ def multExpr: Parser[Expression] =
+ unaryExpr ~ (MulOp ~ unaryExpr *) ^^ {
+ case e0 ~ rest => (rest foldLeft e0) {
+ case (a, "*" ~ b) => Times(a,b)
+ case (a, "/" ~ b) => Div(a,b)
+ case (a, "%" ~ b) => Mod(a,b) }}
+ def MulOp = "*" | "/" | "%"
+ def unaryExpr: Parser[Expression] =
+ ( "!" ~> unaryExpr ^^ Not
+ | "-" ~> unaryExpr ^^ { Minus(IntLiteral(0),_) }
+ | functionApplication
+ | selectExpr
+ )
+ def selectExpr: Parser[Expression] =
+ atom ~ ("." ~> identOrSpecial *) ^^ {
+ case e ~ fields => (fields foldLeft e) { case (e, f) => val result = MemberAccess(e, f); result.pos = e.pos; result }
+ }
+ def selectExprFerSure: Parser[MemberAccess] =
+ 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 functionApplication: Parser[Expression] =
+ atom ~ rep("." ~> identOrSpecial ~ opt("(" ~> repsep(expression, ",") <~ ")")) ^^ {
+ case target ~ members =>
+ members.foldLeft(target)({ case (e, name ~ args) => val result = if(! args.isDefined) MemberAccess(e, name) else FunctionApplication(e, name, args.get); result.pos = e.pos; result })
+ }
+
+ def identOrSpecial: Parser[String] =
+ ( ident ^^ { case s => s }
+ | "acquire" ^^^ "acquire"
+ | "release" ^^^ "release"
+ | "fork" ^^^ "fork"
+ | "*" ^^^ "*")
+
+ var currentLocalVariables = Set[String]()
+
+ def expressionList =
+ expression ~ ("," ~> expression *) ^^ { case e ~ ee => e::ee }
+
+ def atom : Parser[Expression] =
+ positioned( numericLit ^^ { case n => IntLiteral(n.toInt) }
+ | "false" ^^^ BoolLiteral(false)
+ | "true" ^^^ BoolLiteral(true)
+ | "null" ^^^ NullLiteral()
+ | "maxlock" ^^^ MaxLockLiteral()
+ | "lockbottom" ^^^ LockBottomLiteral()
+ | "this" ^^^ ExplicitThisExpr()
+ | ("[" ~> expression) ~ (":" ~> expression <~ "]") ^^ { case from ~ to => Range(from, to) }
+ | "(" ~> expression <~ ")"
+ | ("eval" ~ "(") ~> (evalstate <~ ",") ~ (expression <~ ")") ^^ { case h ~ e => Eval(h, e) }
+ | ("ite(" ~> expression <~ ",") ~ (expression <~ ",") ~ (expression <~ ")") ^^ { case con ~ then ~ els => IfThenElse (con, then, els) }
+ | "rd" ~>
+ ( "holds" ~> "(" ~> expression <~ ")" ^^ RdHolds
+ | "(" ~>
+ ( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result})) ~ rdPermArg <~ ")"
+ | selectExprFerSure ~ rdPermArg <~ ")"
+ ) ^^ { case MemberAccess(obj, "*") ~ p => RdAccessAll(obj, p) case e ~ p => RdAccess(e,p) }
+ )
+ | "acc" ~> "(" ~>
+ ( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result} )) ~ ("," ~> expression ?) <~ ")"
+ | selectExprFerSure ~ ("," ~> expression ?) <~ ")"
+ ) ^^ { case MemberAccess(obj, "*") ~ perm => AccessAll(obj, perm) case e ~ perm => Access(e, perm) }
+ | "holds" ~> "(" ~> expression <~ ")" ^^ Holds
+ | "assigned" ~> "(" ~> ident <~ ")" ^^ Assigned
+ | "old" ~> "(" ~> expression <~ ")" ^^ Old
+ | positioned(Ident) ~ opt("(" ~> repsep(expression, ",") <~ ")") ^^
+ { case id ~ args => val result =
+ if(args.isDefined){
+ val implicitThis = ImplicitThisExpr(); implicitThis.pos = id.pos;
+ FunctionApplication(implicitThis, id.v, args.get)
+ } else {
+ if (currentLocalVariables contains id.v)
+ VariableExpr(id.v)
+ else {
+ val implicitThis = ImplicitThisExpr(); implicitThis.pos = id.pos; MemberAccess(implicitThis, id.v)
+ }
+ }; result.pos = id.pos; result }
+ | ("unfolding" ~> expression <~ "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)
+ }
+ | ("nil" ~> "<") ~> (typeDecl <~ ">") ^^ EmptySeq
+ | ("[" ~> repsep(expression, ",") <~ "]") ^^ { case es => ExplicitSeq(es) }
+ | "|" ~> expression <~ "|" ^^ Length
+ | forall
+ | "result" ^^^ Result()
+ )
+ def forall: Parser[Forall] =
+ (("forall" ~ "{") ~> repsep(ident, ",") <~ "in") into { is => (expression <~ ";") ~ (exprWithLocals(is) <~ "}") ^^
+ { case seq ~ e => val result = Forall(is, seq, e); currentLocalVariables = currentLocalVariables -- is; result } }
+ def exprWithLocals(i: List[String]) : Parser[Expression] = {
+ val savedCurrentLocals = currentLocalVariables;
+ currentLocalVariables = currentLocalVariables ++ i;
+ val result = ((expression) ^^ { case e => e});
+ result
+ }
+
+ def evalstate: Parser[EvalState] = {
+ functionApplication ~ opt(callTarget ~ (repsep(expression, ",") <~ ")")) ^?
+ { case MemberAccess(e, "acquire") ~ None => AcquireState(e)
+ case MemberAccess(e, "release") ~ None => ReleaseState(e)
+ case MemberAccess(e, "fork") ~ Some((MemberAccess(obj, id) ~ args)) => CallState(e, obj, id, args)
+ }
+ }
+
+ def rdPermArg : Parser[Option[Option[Expression]]] =
+ (("," ~> ( "*" ^^^ None
+ | expression ^^ { case e => Some(e) }
+ )) ?
+ )
+}
diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala new file mode 100644 index 00000000..876a5abe --- /dev/null +++ b/Chalice/src/Prelude.scala @@ -0,0 +1,251 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+object TranslatorPrelude {
+
+ val P =
+"""// Copyright (c) 2008, Microsoft
+type Field a;
+type HeapType = <a>[ref,Field a]a;
+type MaskType = <a>[ref,Field a][PermissionComponent]int;
+type ref;
+const null: ref;
+
+var Heap: HeapType;
+
+type PermissionComponent;
+const unique perm$R: PermissionComponent;
+const unique perm$N: PermissionComponent;
+const Permission$MinusInfinity: int;
+axiom Permission$MinusInfinity < -10000;
+const Permission$PlusInfinity: int;
+axiom 10000 < Permission$PlusInfinity;
+var Mask: MaskType where IsGoodMask(Mask);
+const Permission$Zero: [PermissionComponent]int;
+axiom Permission$Zero[perm$R] == 0 && Permission$Zero[perm$N] == 0;
+const Permission$Full: [PermissionComponent]int;
+axiom Permission$Full[perm$R] == 100 && Permission$Full[perm$N] == 0;
+const ZeroMask: MaskType;
+axiom (forall<T> o: ref, f: Field T, pc: PermissionComponent :: ZeroMask[o,f][pc] == 0);
+axiom IsGoodMask(ZeroMask);
+function {:expand false} CanRead<T>(m: MaskType, obj: ref, f: Field T) returns (bool)
+{
+ 0 < m[obj,f][perm$R] || 0 < m[obj,f][perm$N]
+}
+function {:expand false} CanWrite<T>(m: MaskType, obj: ref, f: Field T) returns (bool)
+{
+ m[obj,f][perm$R] == 100 && m[obj,f][perm$N] == 0
+}
+function {:expand true} IsGoodMask(m: MaskType) returns (bool)
+{
+ (forall<T> o: ref, f: Field T ::
+ 0 <= m[o,f][perm$R] &&
+ (NonPredicateField(f) ==>
+ (m[o,f][perm$R]<=100 &&
+ (0 < m[o,f][perm$N] ==> m[o,f][perm$R] < 100))) &&
+ (m[o,f][perm$N] < 0 ==> 0 < m[o,f][perm$R]))
+}
+
+function IsGoodState<T>(T) returns (bool);
+function combine<T,U>(T, U) returns (T);
+const nostate: HeapType;
+
+axiom (forall<T,U> a: T, b: U :: {IsGoodState(combine(a, b))} IsGoodState(combine(a, b)) <==> IsGoodState(a) && IsGoodState(b));
+axiom IsGoodState(nostate);
+
+type ModuleName;
+const CurrentModule: ModuleName;
+type TypeName;
+function dtype(ref) returns (TypeName);
+const CanAssumeFunctionDefs: bool;
+
+type Mu;
+const unique mu: Field Mu;
+axiom NonPredicateField(mu);
+function MuBelow(Mu, Mu) returns (bool); // strict partial order
+axiom (forall m: Mu, n: Mu ::
+ { MuBelow(m,n), MuBelow(n,m) }
+ !(MuBelow(m,n) && MuBelow(n,m)));
+axiom (forall m: Mu, n: Mu, o: Mu ::
+ { MuBelow(m,n), MuBelow(n,o) }
+ MuBelow(m,n) && MuBelow(n,o) ==> MuBelow(m,o));
+const $LockBottom: Mu;
+axiom (forall m, n: Mu :: MuBelow(m, n) ==> n != $LockBottom);
+
+const unique held: Field int;
+function Acquire$Heap(int) returns (HeapType);
+function Acquire$Mask(int) returns (MaskType);
+axiom NonPredicateField(held);
+
+function LastSeen$Heap(Mu, int) returns (HeapType);
+function LastSeen$Mask(Mu, int) returns (MaskType);
+
+const unique rdheld: Field bool;
+axiom NonPredicateField(rdheld);
+function wf(h: HeapType, m: MaskType) returns (bool);
+
+function IsGoodInhaleState(ih: HeapType, h: HeapType,
+ m: MaskType) returns (bool)
+{
+ (forall<T> o: ref, f: Field T :: { ih[o, f] } CanRead(m, o, f) ==> ih[o, f] == h[o, f]) &&
+ (forall o: ref :: { ih[o, held] } (0<ih[o, held]) == (0<h[o, held])) &&
+ (forall o: ref :: { ih[o, rdheld] } ih[o, rdheld] == h[o, rdheld]) &&
+ (forall o: ref :: { h[o, held] } (0<h[o, held]) ==> ih[o, mu] == h[o, mu])
+}
+
+function ite<T>(bool, T, T) returns (T);
+axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} con ==> ite(con, a, b) == a);
+axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} ! con ==> ite(con, a, b) == b);
+
+type Seq T;
+
+function Seq#Length<T>(Seq T) returns (int);
+axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));
+
+function Seq#Empty<T>() returns (Seq T);
+axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);
+axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());
+
+function Seq#Singleton<T>(T) returns (Seq T);
+axiom (forall<T> t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1);
+
+function Seq#Build<T>(s: Seq T, index: int, val: T, newLength: int) returns (Seq T);
+axiom (forall<T> s: Seq T, i: int, v: T, len: int :: { Seq#Length(Seq#Build(s,i,v,len)) }
+ Seq#Length(Seq#Build(s,i,v,len)) == len);
+
+function Seq#Append<T>(Seq T, Seq T) returns (Seq T);
+axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) }
+ Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1));
+
+function Seq#Index<T>(Seq T, int) returns (T);
+axiom (forall<T> t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t);
+axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) }
+ (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) &&
+ (Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, n - Seq#Length(s0))));
+axiom (forall<T> s: Seq T, i: int, v: T, len: int, n: int :: { Seq#Index(Seq#Build(s,i,v,len),n) }
+ (i == n ==> Seq#Index(Seq#Build(s,i,v,len),n) == v) &&
+ (i != n ==> Seq#Index(Seq#Build(s,i,v,len),n) == Seq#Index(s,n)));
+
+function Seq#Contains<T>(Seq T, T) returns (bool);
+axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
+ Seq#Contains(s,x) <==>
+ (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x));
+axiom (forall x: ref ::
+ { Seq#Contains(Seq#Empty(), x) }
+ !Seq#Contains(Seq#Empty(), x));
+axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::
+ { Seq#Contains(Seq#Append(s0, s1), x) }
+ Seq#Contains(Seq#Append(s0, s1), x) <==>
+ Seq#Contains(s0, x) || Seq#Contains(s1, x));
+axiom (forall<T> s: Seq T, i: int, v: T, len: int, x: T ::
+ { Seq#Contains(Seq#Build(s, i, v, len), x) }
+ Seq#Contains(Seq#Build(s, i, v, len), x) <==>
+ x == v || Seq#Contains(s, x));
+axiom (forall<T> s: Seq T, n: int, x: T ::
+ { Seq#Contains(Seq#Take(s, n), x) }
+ Seq#Contains(Seq#Take(s, n), x) <==>
+ (exists i: int :: { Seq#Index(s, i) }
+ 0 <= i && i < n && n <= Seq#Length(s) && Seq#Index(s, i) == x));
+axiom (forall<T> s: Seq T, n: int, x: T ::
+ { Seq#Contains(Seq#Drop(s, n), x) }
+ Seq#Contains(Seq#Drop(s, n), x) <==>
+ (exists i: int :: { Seq#Index(s, i) }
+ 0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));
+
+function Seq#Equal<T>(Seq T, Seq T) returns (bool);
+axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }
+ Seq#Equal(s0,s1) <==>
+ Seq#Length(s0) == Seq#Length(s1) &&
+ (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
+ 0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
+axiom(forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a,b) } // extensionality axiom for sequences
+ Seq#Equal(a,b) ==> a == b);
+
+function Seq#SameUntil<T>(Seq T, Seq T, int) returns (bool);
+axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0,s1,n) }
+ Seq#SameUntil(s0,s1,n) <==>
+ (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
+ 0 <= j && j < n ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
+
+function Seq#Take<T>(Seq T, howMany: int) returns (Seq T);
+axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) }
+ 0 <= n ==>
+ (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&
+ (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)));
+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) }
+ 0 <= j && j < n && j < Seq#Length(s) ==>
+ Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));
+
+function Seq#Drop<T>(Seq T, howMany: int) returns (Seq T);
+axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) }
+ 0 <= n ==>
+ (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&
+ (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0));
+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) }
+ 0 <= n && 0 <= j && j < Seq#Length(s)-n ==>
+ Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));
+
+function Seq#Range(min: int, max: int) returns (Seq int);
+
+axiom (forall min: int, max: int :: { Seq#Length(Seq#Range(min, max)) } (min < max ==> Seq#Length(Seq#Range(min, max)) == max-min) && (max <= min ==> Seq#Length(Seq#Range(min, max)) == 0));
+axiom (forall min: int, max: int, j: int :: { Seq#Index(Seq#Range(min, max), j) } 0<=j && j<max-min ==> Seq#Index(Seq#Range(min, max), j) == min + j);
+
+axiom (forall h: HeapType, m: MaskType, o: ref, q: ref :: {wf(h, m), h[o, mu], h[q, mu]} wf(h, m) && o!=q && (0 < h[o, held]) && (0 < h[q, held]) ==> h[o, mu] != h[q, mu]);
+
+function DecPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$R]}
+ DecPerm(m, o, f, howMuch)[q, g][perm$R] == ite(o==q && f ==g, m[q, g][perm$R] - howMuch, m[q, g][perm$R])
+);
+
+function DecEpsilons<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$N]}
+ DecEpsilons(m, o, f, howMuch)[q, g][perm$N] == ite(o==q && f ==g, m[q, g][perm$N] - howMuch, m[q, g][perm$N])
+);
+
+function IncPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$R]}
+ IncPerm(m, o, f, howMuch)[q, g][perm$R] == ite(o==q && f ==g, m[q, g][perm$R] + howMuch, m[q, g][perm$R])
+);
+
+function IncEpsilons<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$N]}
+ IncEpsilons(m, o, f, howMuch)[q, g][perm$N] == ite(o==q && f ==g, m[q, g][perm$N] + howMuch, m[q, g][perm$N])
+);
+
+function Havocing<T,U>(h: HeapType, o: ref, f: Field T, newValue: U) returns (HeapType);
+
+axiom (forall<T,U> h: HeapType, o: ref, f: Field T, newValue: U, q: ref, g: Field U :: {Havocing(h, o, f, newValue)[q, g]}
+ Havocing(h, o, f, newValue)[q, g] == ite(o==q && f ==g, newValue, h[q, g])
+);
+
+const unique joinable: Field int;
+axiom NonPredicateField(joinable);
+const unique token#t: TypeName;
+
+function Call$Heap(int) returns (HeapType);
+function Call$Mask(int) returns (MaskType);
+function Call$Args(int) returns (ArgSeq);
+type ArgSeq = <T>[int]T;
+
+function EmptyMask(m: MaskType) returns (bool);
+axiom (forall m: MaskType :: {EmptyMask(m)} EmptyMask(m) <==> (forall<T> o: ref, f: Field T :: NonPredicateField(f) ==> m[o, f][perm$R]<=0 && m[o, f][perm$N]<=0));
+
+function NonPredicateField<T>(f: Field T) returns (bool);
+function PredicateField<T>(f: Field T) returns (bool);
+axiom (forall<T> f: Field T :: NonPredicateField(f) ==> ! PredicateField(f));
+axiom (forall<T> f: Field T :: PredicateField(f) ==> ! NonPredicateField(f));
+
+function submask(m1: MaskType, m2: MaskType) returns (bool);
+
+axiom (forall m1: MaskType, m2: MaskType :: {submask(m1, m2)}
+ submask(m1, m2) <==> (forall<T> o: ref, f: Field T :: (m1[o, f][perm$R] < m2[o, f][perm$R]) || (m1[o, f][perm$R] == m2[o, f][perm$R] && m1[o, f][perm$N] <= m2[o, f][perm$N]))
+);
+
+"""
+}
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala new file mode 100644 index 00000000..b93c23bd --- /dev/null +++ b/Chalice/src/PrettyPrinter.scala @@ -0,0 +1,292 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+object PrintProgram {
+ def P(prog: List[Class]) =
+ for (cl <- prog) {
+ if (cl.IsExternal) print("external ")
+ println("class " + cl.id + " module " + cl.module + " {")
+ cl.members foreach Member
+ println("}")
+ }
+ def Semi = ";"
+ def Member(m: Member) = m match {
+ 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)
+ case m: Method =>
+ print(" method " + m.id)
+ print("("); VarList(m.ins); print(")")
+ if (m.outs != Nil) {
+ print(" returns ("); VarList(m.outs); print(")")
+ }
+ println
+ m.spec foreach {
+ case Precondition(e) => print(" requires "); Expr(e); println(Semi)
+ case Postcondition(e) => print(" ensures "); Expr(e); println(Semi)
+ case LockChange(ee) => print(" lockchange "); ExprList(ee); println(Semi)
+ }
+ println(" {");
+ for (s <- m.body) {
+ print(" "); Stmt(s, 4)
+ }
+ println(" }")
+ case Predicate(id, definition) =>
+ print(" predicate " + id + " { " + Expr(definition) + "}")
+ case Function(id, ins, out, specs, e) =>
+ print(" function " + id + "(" + VarList(ins) + ")" + ": " + out.id);
+ specs foreach {
+ case Precondition(e) => print(" requires "); Expr(e); println(Semi)
+ case Postcondition(e) => print(" ensures "); Expr(e); println(Semi)
+ case LockChange(ee) => print(" lockchange "); ExprList(ee); println(Semi)
+ }
+ print(" { " + Expr(e) + "}");
+ }
+ def Stmt(s: Statement, indent: int): unit = s match {
+ case Assert(e) =>
+ print("assert "); Expr(e); println(Semi)
+ case Assume(e) =>
+ print("assume "); Expr(e); println(Semi)
+ case BlockStmt(ss) =>
+ PrintBlockStmt(ss, indent); println
+ case IfStmt(guard, BlockStmt(thn), els) =>
+ print("if ("); Expr(guard); print(") ")
+ PrintBlockStmt(thn, indent)
+ els match {
+ case None => println
+ case Some(s) => print(" else "); Stmt(s, indent)
+ }
+ case WhileStmt(guard, invs, lkch, body) =>
+ print("while ("); Expr(guard); println(")")
+ for (inv <- invs) {
+ Spaces(indent+2)
+ print("invariant "); Expr(inv); println(Semi)
+ }
+ for (l <- lkch) {
+ Spaces(indent+2)
+ print("lockchange "); Expr(l); println(Semi)
+ }
+ Spaces(indent); Stmt(body, indent)
+ case Assign(lhs,rhs) =>
+ Expr(lhs); print(" := "); Rhs(rhs); println(Semi)
+ case FieldUpdate(lhs,rhs) =>
+ Expr(lhs); print(" := "); Rhs(rhs); println(Semi)
+ case LocalVar(id,t,c,g,rhs) =>
+ if (g) print("ghost ")
+ if (c) print("const ") else print("var ")
+ print(id + ": " + t.id)
+ rhs match { case None => case Some(rhs) => print(" := "); Rhs(rhs) }
+ println(Semi)
+ case Call(outs, obj, id, args) =>
+ print("call ")
+ outs match {
+ case Nil =>
+ case x :: xs => Expr(x); xs foreach { x => print(", "); Expr(x) }; print(" := ")
+ }
+ MemberSelect(obj,id,0,false)
+ print("(")
+ ExprList(args)
+ println(");")
+ case Install(obj,lower,upper) =>
+ print("reorder ")
+ Expr(obj)
+ PrintBounds(lower, upper)
+ println(Semi)
+ case Share(obj,lower,upper) =>
+ print("share ")
+ Expr(obj)
+ PrintBounds(lower, upper)
+ println(Semi)
+ case Unshare(e) =>
+ print("unshare "); Expr(e); println(Semi)
+ case Acquire(e) =>
+ print("acquire "); Expr(e); println(Semi)
+ case Release(e) =>
+ print("release "); Expr(e); println(Semi)
+ case RdAcquire(e) =>
+ print("rd acquire "); Expr(e); println(Semi)
+ case RdRelease(e) =>
+ print("rd release "); Expr(e); println(Semi)
+ case Lock(e, b, rdLock) =>
+ if (rdLock) print("rd lock (") else print("lock (")
+ Expr(e); print(") ")
+ Stmt(b, indent)
+ case Downgrade(e) =>
+ print("downgrade "); Expr(e); println(Semi)
+ case Free(e) =>
+ print("free "); Expr(e); println(Semi)
+ case Fold(e) =>
+ print("fold "); Expr(e); println(Semi)
+ case Unfold(e) =>
+ print("unfold "); Expr(e); println(Semi)
+ case CallAsync(declaresLocal, token, obj, name, args) =>
+ print("call async ");
+ if (token != null) {
+ Expr(token); print(" := ");
+ }
+ Expr(obj); print("."); print(name); print("("); ExprList(args); print(")");
+ case JoinAsync(lhs, token) =>
+ print("join async "); ExprList(lhs); print(" := "); Expr(token);
+ }
+ def PrintBounds(lower: List[Expression], upper: List[Expression]) = {
+ if (lower == Nil && upper == Nil) {
+ } else if (lower == Nil) {
+ print(" below "); ExprList(upper)
+ } else if (upper == Nil) {
+ print(" above "); ExprList(lower)
+ } else {
+ print(" between "); ExprList(lower); print(" and "); ExprList(upper)
+ }
+ }
+ def PrintBlockStmt(ss: List[Statement], indent: int) = {
+ println("{")
+ for (s <- ss) { Spaces(indent+2); Stmt(s, indent+2) }
+ Spaces(indent); print("}")
+ }
+ 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) }
+ }
+ def ExprList(ee: List[Expression]) = ee match {
+ case Nil =>
+ case e :: rest =>
+ Expr(e)
+ rest foreach { e => print(", "); Expr(e) }
+ }
+ def Rhs(e: RValue) = e match {
+ case NewRhs(id, initialization) =>
+ print("new " + id);
+ if(0 < initialization.length) {
+ print(" {"); print(initialization(0).id); print(":="); Expr(initialization(0).e); initialization.foreach({ init => print(", "); print(init.id); print(":="); Expr(init.e); }); print("}");
+ }
+ case e: Expression => Expr(e)
+ }
+ def Expr(e: Expression): Unit = Expr(e, 0, false)
+ def Expr(e: Expression, contextBindingPower: int, fragileContext: boolean): Unit = e match {
+ case IntLiteral(n) => print(n)
+ case BoolLiteral(b) => print(b)
+ case NullLiteral() => print("null")
+ case MaxLockLiteral() => print("maxlock")
+ case LockBottomLiteral() => print("lockbottom")
+ case _:ThisExpr => print("this")
+ case _:Result => print("result")
+ case VariableExpr(id) => print(id)
+ case MemberAccess(e,f) => MemberSelect(e,f,contextBindingPower,fragileContext)
+ case Access(e,perm) =>
+ print("acc("); Expr(e)
+ perm match { case None => case Some(perm) => print(", "); Expr(perm) }
+ print(")")
+ case RdAccess(e,p) =>
+ print("rd("); Expr(e)
+ p match {
+ case None => print(")")
+ case Some(None) => print(", *)")
+ case Some(Some(e)) => print(", "); Expr(e); print(")")
+ }
+ case AccessAll(obj, perm) =>
+ print("acc("); Expr(obj); print(".*");
+ perm match { case None => case Some(perm) => print(", "); Expr(perm) }
+ print(")")
+ case RdAccessAll(obj, p) =>
+ print("rd("); Expr(e); print(".*");
+ p match {
+ case None => print(")")
+ case Some(None) => print(", *)")
+ case Some(Some(e)) => print(", "); Expr(e); print(")")
+ }
+ case Holds(e) =>
+ print("holds("); Expr(e); print(")")
+ case RdHolds(e) =>
+ print("rd holds("); Expr(e); print(")")
+ case Assigned(id) => print("assigned(" + id + ")")
+ case Old(e) =>
+ print("old("); Expr(e); print(")")
+ case IfThenElse(con, then, els) =>
+ print("ite("); Expr(con); print(", "); Expr(then); print(", "); Expr(els); print(")");
+ case Not(e) => print("!"); Expr(e, 0x80, false)
+ case FunctionApplication(obj, id, ins) =>
+ Expr(obj); print("."); print(id); print("("); ExprList(ins); print(")");
+ case Unfolding(pred, e) =>
+ print("unfolding "); Expr(pred); print(" in "); Expr(e);
+ case e:Iff => BinExpr(e, e.OpName, 0x10, false, false, contextBindingPower, fragileContext)
+ case e:Implies => BinExpr(e, e.OpName, 0x20, true, false, contextBindingPower, fragileContext)
+ case e:And => BinExpr(e, e.OpName, 0x30, false, false, contextBindingPower, fragileContext)
+ case e:Or => BinExpr(e, e.OpName, 0x31, false, false, contextBindingPower, fragileContext)
+ case e:Eq => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
+ case e:Neq => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
+ case e:Less => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
+ case e:AtMost => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
+ case e:AtLeast => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
+ case e:Greater => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
+ case e:LockBelow => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
+ case e:Plus => BinExpr(e, e.OpName, 0x50, false, false, contextBindingPower, fragileContext)
+ case e:Minus => BinExpr(e, e.OpName, 0x50, false, true, contextBindingPower, fragileContext)
+ case e:Times => BinExpr(e, e.OpName, 0x60, false, false, contextBindingPower, fragileContext)
+ case e:Div => BinExpr(e, e.OpName, 0x60, false, true, contextBindingPower, fragileContext)
+ case e:Mod => BinExpr(e, e.OpName, 0x60, false, true, contextBindingPower, fragileContext)
+ case q:Quantification =>
+ print(q.Quantor + "{");
+ q.Is match {
+ case Nil =>
+ case i :: rest => print(i); rest foreach { v => print(", " + v) }
+ }
+ print(" in "); Expr(q.Seq); print("; "); Expr(q.E); print("}");
+ case EmptySeq(t) =>
+ print("nil<"); print(t.FullName); print(">");
+ case ExplicitSeq(es) =>
+ print("["); ExprList(es); print("]");
+ case Range(min, max) =>
+ print("("); Expr(min); print(":"); Expr(max); print(")");
+ case Length(e)=>
+ print("|"); Expr(e); print("|");
+ case e:At =>
+ BinExpr(e, e.OpName, 0x45, true, true, contextBindingPower, fragileContext)
+ case e:Append =>
+ BinExpr(e, e.OpName, 0x45, true, true, contextBindingPower, fragileContext)
+ case Drop(s, n) =>
+ Expr(s); print("["); Expr(n); print(" ..]");
+ case Take(s, n) =>
+ Expr(s); print("[.. "); Expr(n); print("]");
+ case Eval(h, e) =>
+ print("eval("); (h match
+ {
+ case AcquireState(obj) => Expr(obj); print(".acquire");
+ case ReleaseState(obj) => Expr(obj); print(".release");
+ case CallState(token, obj, id, args) => Expr(token); print(".joinable"); print(", "); Expr(obj); print("." + id + "("); ExprList(args); print(")");
+ }); print(", "); Expr(e); print(")");
+ }
+ def MemberSelect(e: Expression, f: String, contextBindingPower: int, fragileContext: boolean) = e match {
+ case e:ImplicitThisExpr => print(f)
+ case _ =>
+ ParenExpr(0x90, contextBindingPower, fragileContext, { Expr(e,0x90,false); print("." + f) })
+ }
+ def BinExpr(bin: BinaryExpr, op: String, power: int, fragileLeft: boolean, fragileRight: boolean,
+ context: int, fragileContext: boolean) = {
+ ParenExpr(power, context, fragileContext,
+ { Expr(bin.E0, power, fragileLeft); print(" " + op + " "); Expr(bin.E1, power, fragileRight) })
+ }
+ def ParenExpr(power: int, context: int, fragileContext: boolean, pe: =>Unit) {
+ val ap = power & 0xF0;
+ val cp = context & 0xF0;
+ val parensNeeded = ap < cp || (ap == cp && (power != context || fragileContext));
+ if (parensNeeded) { print("(") }
+ pe
+ if (parensNeeded) { print(")") }
+ }
+ def Spaces(N: int) = {
+ val abunchaSpaces = " "
+ var n = N
+ while (abunchaSpaces.length <= n) {
+ print(abunchaSpaces)
+ n = n - abunchaSpaces.length
+ }
+ if (0 < n) {
+ print(abunchaSpaces.substring(0, n))
+ }
+ }
+}
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala new file mode 100644 index 00000000..c7bdfd15 --- /dev/null +++ b/Chalice/src/Resolver.scala @@ -0,0 +1,940 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+import scala.util.parsing.input.Position
+import scala.util.parsing.input.Positional
+
+object Resolver {
+ sealed abstract class ResolverOutcome
+ case class Success extends ResolverOutcome
+ case class Error(pos: Position, s: String) extends ResolverOutcome
+ case class Errors(ss: List[String]) extends ResolverOutcome
+
+ var seqClasses = Map[String, SeqClass]();
+
+ class ProgramContext(classes: Map[String,Class], currentClass: Class) {
+ val Classes = classes
+ val CurrentClass = currentClass
+ var currentMember = null: Member;
+ def CurrentMember = currentMember: Member;
+ var errors: List[String] = Nil
+ def Error(pos: Position, msg: String) {
+ errors = errors + (pos + ": " + msg)
+ }
+ def AddVariable(v: Variable): ProgramContext = {
+ new LProgramContext(v, this);
+ }
+ def LookupVariable(id: String): Option[Variable] = None
+ def IsVariablePresent(vr: Variable): boolean = false
+
+ private class LProgramContext(v: Variable, parent: ProgramContext) extends ProgramContext(parent.Classes, parent.CurrentClass) {
+ override def Error(pos: Position, msg: String) = parent.Error(pos, msg)
+ override def LookupVariable(id: String): Option[Variable] = {
+ if (id == v.id) Some(v) else parent.LookupVariable(id)
+ }
+ override def IsVariablePresent(vr: Variable): boolean = {
+ if (vr == v) true else parent.IsVariablePresent(vr)
+ }
+ override def CurrentMember() = {
+ parent.CurrentMember
+ }
+ }
+ }
+
+ def Resolve(prog: List[Class]): ResolverOutcome = {
+ // register the classes and their members
+ var classes = Map[String,Class]()
+ for (cl <- BoolClass :: IntClass :: RootClass :: NullClass :: MuClass :: prog) {
+ if (classes contains cl.id) {
+ return Error(cl.pos, "duplicate class name: " + cl.id)
+ } else {
+ for (m <- cl.members) m match {
+ case _:MonitorInvariant =>
+ case m: NamedMember =>
+ m.Parent = cl
+ if (cl.mm contains m.Id) {
+ return Error(m.pos, "duplicate member name " + m.Id + " in class " + cl.id)
+ } else {
+ cl.mm = cl.mm + (m.Id -> m)
+ }
+ }
+ classes = classes + (cl.id -> cl)
+ }
+ }
+ var errors = List[String]()
+
+ // resolve types of fields and methods
+ val contextNoCurrentClass = new ProgramContext(classes, null)
+ for (cl <- prog; m <- cl.members) m match {
+ case _:MonitorInvariant =>
+ case Field(id,t) =>
+ ResolveType(t, contextNoCurrentClass)
+ case Method(id, ins, outs, spec, body) =>
+ for (v <- ins ++ outs) {
+ ResolveType(v.t, contextNoCurrentClass)
+ }
+ case Predicate(id, definition) =>
+ case Function(id, ins, out, specs, definition) =>
+ for (v <- ins) {
+ ResolveType(v.t, contextNoCurrentClass)
+ }
+ ResolveType(out, contextNoCurrentClass)
+ }
+ errors = errors ++ contextNoCurrentClass.errors;
+
+ // now, resolve and typecheck all
+ // * Field types and Method formal-parameter types
+ // * Assign, FieldUpdate, and Call statements
+ // * VariableExpr and FieldSelect expressions
+ for (cl <- prog) {
+ val context = new ProgramContext(classes, cl)
+ for (m <- cl.members) {
+ context.currentMember = m;
+ m match {
+ case MonitorInvariant(e) =>
+ ResolveExpr(e, context, true, true)(true)
+ if (!e.typ.IsBool) context.Error(m.pos, "monitor invariant requires a boolean expression (found " + e.typ.FullName + ")")
+ case _:Field => // nothing more to do
+ case m@Method(id, ins, outs, spec, body) =>
+ var ctx = context
+ for (v <- ins ++ outs) {
+ ctx = ctx.AddVariable(v)
+ }
+ spec foreach {
+ case Precondition(e) => ResolveExpr(e, ctx, false, true)(false)
+ case Postcondition(e) => ResolveExpr(e, ctx, true, true)(false)
+ case lc@LockChange(ee) =>
+ if(m.id.equals("run")) context.Error(lc.pos, "lockchange not allowed on method run")
+ ee foreach (e => ResolveExpr(e, ctx, true, false)(false))
+ }
+ ResolveStmt(BlockStmt(body), ctx)
+ case p@Predicate(id, e) =>
+ var ctx = context;
+ ResolveExpr(e, ctx, false, true)(true);
+ if(!e.typ.IsBool) context.Error(e.pos, "predicate requires a boolean expression (found " + e.typ.FullName + ")")
+ case f@Function(id, ins, out, spec, e) =>
+ var ctx = context
+ for (v <- ins) {
+ ctx = ctx.AddVariable(v)
+ }
+ spec foreach {
+ case Precondition(e) => ResolveExpr(e, ctx, false, true)(false)
+ case pc@Postcondition(e) => assert(ctx.CurrentMember != null); ResolveExpr(e, ctx, false, true)(false)
+ case lc@LockChange(ee) => context.Error(lc.pos, "lockchange not allowed on function")
+ }
+ ResolveExpr(e, ctx, false, false)(false)
+ if(! canAssign(out.typ, e.typ)) context.Error(e.pos, "function body does not match declared type (expected: " + out.FullName + ", found: " + e.typ.FullName + ")")
+ }
+ }
+ errors = errors ++ context.errors
+ }
+
+ if (errors.length == 0) {
+ Success()
+ } else {
+ Errors(errors)
+ }
+ }
+
+ def ResolveType(t: Type, context: ProgramContext): unit = {
+ for(p <- t.params){
+ ResolveType(p, context);
+ }
+ if(t.isInstanceOf[TokenType]){
+ val tt = t.asInstanceOf[TokenType];
+ ResolveType(tt.C, context);
+ if(! tt.C.typ.IsNormalClass) context.Error(t.pos, "Invalid token type. " + tt.C.FullName + " is not a user-defined class.");
+ tt.C.typ.LookupMember(tt.m) match {
+ case Some(m: Method) => val tc = TokenClass(tt.C, tt.m); tc.method = m; tt.typ = tc;
+ case _ => context.Error(t.pos, "Invalid token type. " + tt.C.FullName + " does not declare a method " + tt.m + ".");
+ }
+ return;
+ }
+ if (context.Classes contains t.FullName) {
+ t.typ = context.Classes(t.FullName)
+ } else {
+ if(seqClasses.contains(t.FullName)) {
+ t.typ = seqClasses(t.FullName)
+ } else if(t.id.equals("seq") && t.params.length == 1) {
+ val seqt = new SeqClass(t.params(0).typ);
+ seqClasses = seqClasses + ((seqt.FullName, seqt));
+ t.typ = seqt;
+ } else {
+ context.Error(t.pos, "undeclared type " + t.FullName)
+ t.typ = IntClass
+ }
+ }
+ }
+
+ def getSeqType(param: Class, context: ProgramContext): Class = {
+ if(seqClasses.contains("seq<" + param.FullName + ">")) {
+ seqClasses("seq<" + param.FullName + ">")
+ } else {
+ val seqt = new SeqClass(param);
+ seqClasses = seqClasses + ((seqt.FullName, seqt));
+ seqt
+ }
+ }
+
+ def ResolveStmt(s: Statement, context: ProgramContext): unit = s match {
+ case Assert(e) =>
+ ResolveExpr(e, context, true, true)(false)
+ if (!e.typ.IsBool) context.Error(e.pos, "assert statement requires a boolean expression (found " + e.typ.FullName + ")")
+ case Assume(e) =>
+ ResolveExpr(e, context, false, false)(false) // assume expressions remain at run-time, so OLD is not allowed
+ if (!e.typ.IsBool) context.Error(e.pos, "assume statement requires a boolean expression (found " + e.typ.FullName + ")")
+ CheckNoGhost(e, context)
+ case BlockStmt(ss) =>
+ var ctx = context
+ for (s <- ss) s match {
+ case l @ LocalVar(id, t, c, g, rhs) =>
+ ResolveType(l.v.t, ctx)
+ val oldCtx = ctx
+ ctx = ctx.AddVariable(l.v)
+ rhs match {
+ case None =>
+ case Some(rhs) =>
+ val lhs = VariableExpr(id)
+ lhs.pos = l.pos;
+ ResolveExpr(lhs, ctx, false, false)(false)
+ ResolveAssign(lhs, rhs, oldCtx)
+ }
+ case c@CallAsync(declaresLocal, token, obj, id, args) =>
+ ResolveStmt(c, ctx)
+ if (declaresLocal) {
+ c.local = new Variable(token.id, TokenType(new Type(obj.typ), id))
+ ResolveType(c.local.t, ctx)
+ ctx = ctx.AddVariable(c.local)
+ ResolveExpr(token, ctx, false, false)(false)
+ }
+ case s =>
+ ResolveStmt(s, ctx)
+ }
+ case IfStmt(guard, thn, els) =>
+ ResolveExpr(guard, context, false, false)(false)
+ if (!guard.typ.IsBool) context.Error(guard.pos, "if statement requires a boolean guard (found " + guard.typ.FullName + ")")
+ CheckNoGhost(guard, context)
+ ResolveStmt(thn, context)
+ els match { case None => case Some(s) => ResolveStmt(s, context) }
+ case w@ WhileStmt(guard, invs, lkch, body) =>
+ ResolveExpr(guard, context, false, false)(false)
+ if (!guard.typ.IsBool) context.Error(guard.pos, "while statement requires a boolean guard (found " + guard.typ.FullName + ")")
+ CheckNoGhost(guard, context)
+ for (inv <- invs) {
+ ResolveExpr(inv, context, true, true)(false)
+ if (!inv.typ.IsBool) context.Error(inv.pos, "loop invariant must be boolean (found " + inv.typ.FullName + ")")
+ }
+ for (l <- lkch) {
+ ResolveExpr(l, context, true, false)(false)
+ if (!l.typ.IsRef) context.Error(l.pos, "lockchange expression must be reference (found " + l.typ.FullName + ")")
+ }
+ ResolveStmt(body, context)
+ w.LoopTargets = ComputeLoopTargets(body) filter context.IsVariablePresent
+ case Assign(lhs, rhs) =>
+ ResolveExpr(lhs, context, false, false)(false)
+ ResolveAssign(lhs, rhs, context)
+ if (lhs.v != null && lhs.v.IsImmutable) {
+ if (lhs.v.IsGhost)
+ CheckNoGhost(rhs, context)
+ else
+ context.Error(lhs.pos, "cannot assign to immutable variable " + lhs.v.id)
+ }
+ case fu@FieldUpdate(lhs, rhs) =>
+ ResolveExpr(lhs, context, false, false)(false)
+ if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(lhs.e, context)
+ if (! lhs.isPredicate && lhs.f.isInstanceOf[SpecialField]) context.Error(lhs.pos, "cannot assign directly to special field: " + lhs.id)
+ ResolveExpr(rhs, context, false, false)(false)
+ if (! lhs.isPredicate && !canAssign(lhs.typ, rhs.typ)) context.Error(fu.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)
+ if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(rhs, context)
+ case lv:LocalVar => throw new Exception("unexpected LocalVar; should have been handled in BlockStmt above")
+ case c @ Call(lhs, obj, id, args) =>
+ ResolveExpr(obj, context, false, false)(false)
+ CheckNoGhost(obj, context)
+ args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }
+ var vars = Set[Variable]()
+ for (v <- lhs) {
+ ResolveExpr(v, context, false, false)(false)
+ if (v.v != null) {
+ if (v.v.IsImmutable) context.Error(v.pos, "cannot use immutable variable " + v.id + " as actual out-parameter")
+ if (vars contains v.v) {
+ context.Error(v.pos, "duplicate actual out-parameter: " + v.id)
+ } else {
+ vars = vars + v.v
+ }
+ }
+ }
+ // lookup method
+ var typ: Class = IntClass
+ obj.typ.LookupMember(id) match {
+ case None =>
+ context.Error(c.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)
+ case Some(m: Method) =>
+ c.m = m
+ if (args.length != m.ins.length)
+ context.Error(c.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +
+ " (" + args.length + " instead of " + m.ins.length + ")")
+ else {
+ for((actual, formal) <- args zip m.ins){
+ if(! canAssign(formal.t.typ, actual.typ))
+ context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")
+ }
+ }
+ if (lhs.length != m.outs.length)
+ context.Error(c.pos, "wrong number of actual out-parameters in call to " + obj.typ.FullName + "." + id +
+ " (" + lhs.length + " instead of " + m.outs.length + ")")
+ else {
+ for((out, l) <- m.outs zip lhs){
+ if(! canAssign(l.typ, out.t.typ))
+ context.Error(l.pos, "the out parameter cannot be assigned to the lhs (expected: " + l.typ.FullName + ", found: " + out.t.FullName + ")")
+ }
+ }
+
+ case _ => context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)
+ }
+ case Install(obj, lowerBounds, upperBounds) =>
+ ResolveExpr(obj, context, false, false)(false)
+ if (!obj.typ.IsRef) context.Error(obj.pos, "object in install statement must be of a reference type (found " + obj.typ.FullName + ")")
+ for (b <- lowerBounds ++ upperBounds) {
+ ResolveExpr(b, context, true, false)(false)
+ if (!b.typ.IsRef && !b.typ.IsMu) context.Error(b.pos, "install bound must be of a reference type or Mu type" +
+ " (found " + b.typ.FullName + ")")
+ }
+ case Share(obj, lowerBounds, upperBounds) =>
+ ResolveExpr(obj, context, false, false)(false)
+ CheckNoGhost(obj, context)
+ if (!obj.typ.IsRef) context.Error(obj.pos, "object in share statement must be of a reference type (found " + obj.typ.FullName + ")")
+ for (b <- lowerBounds ++ upperBounds) {
+ ResolveExpr(b, context, true, false)(false)
+ if (!b.typ.IsRef && !b.typ.IsMu) context.Error(b.pos, "share bound must be of a reference type or Mu type" +
+ " (found " + b.typ.FullName + ")")
+ }
+ case Unshare(obj) =>
+ ResolveExpr(obj, context, false, false)(false)
+ CheckNoGhost(obj, context)
+ if (!obj.typ.IsRef) context.Error(obj.pos, "object in unshare statement must be of a reference type (found " + obj.typ.FullName + ")")
+ case Acquire(obj) =>
+ ResolveExpr(obj, context, false, false)(false)
+ CheckNoGhost(obj, context)
+ if (!obj.typ.IsRef) context.Error(obj.pos, "object in acquire statement must be of a reference type (found " + obj.typ.FullName + ")")
+ case Release(obj) =>
+ ResolveExpr(obj, context, false, false)(false)
+ CheckNoGhost(obj, context)
+ if (!obj.typ.IsRef) context.Error(obj.pos, "object in release statement must be of a reference type (found " + obj.typ.FullName + ")")
+ case RdAcquire(obj) =>
+ ResolveExpr(obj, context, false, false)(false)
+ CheckNoGhost(obj, context)
+ if (!obj.typ.IsRef) context.Error(obj.pos, "object in rd acquire statement must be of a reference type (found " + obj.typ.FullName + ")")
+ case RdRelease(obj) =>
+ ResolveExpr(obj, context, false, false)(false)
+ CheckNoGhost(obj, context)
+ if (!obj.typ.IsRef) context.Error(obj.pos, "object in rd release statement must be of a reference type (found " + obj.typ.FullName + ")")
+ case Lock(obj, b, rdLock) =>
+ ResolveExpr(obj, context, false, false)(false)
+ CheckNoGhost(obj, context)
+ if (!obj.typ.IsRef) {
+ val sname = if (rdLock) "rd lock" else "lock";
+ context.Error(obj.pos, "object in " + sname + " statement must be of a reference type (found " + obj.typ.FullName + ")")
+
+ }
+ ResolveStmt(b, context)
+ case Downgrade(obj) =>
+ ResolveExpr(obj, context, false, false)(false)
+ CheckNoGhost(obj, context)
+ if (!obj.typ.IsRef) context.Error(obj.pos, "object in downgrade statement must be of a reference type (found " + obj.typ.FullName + ")")
+ case Free(obj) =>
+ ResolveExpr(obj, context, false, false)(false)
+ CheckNoGhost(obj, context)
+ if (!obj.typ.IsRef) context.Error(obj.pos, "object in free statement must be of a reference type (found " + obj.typ.FullName + ")")
+ case fld@Fold(e) =>
+ ResolveExpr(e, context, false, true)(false);
+ CheckNoGhost(e, context);
+ if(!e.getMemberAccess.isPredicate) context.Error(fld.pos, "Fold can only be applied to predicates.")
+ case ufld@Unfold(e) =>
+ ResolveExpr(e, context, false, true)(false);
+ CheckNoGhost(e, context);
+ if(!e.getMemberAccess.isPredicate) context.Error(ufld.pos, "Unfold can only be applied to predicates.")
+ case c@CallAsync(declaresLocal, token, obj, id, args) =>
+ // resolve receiver
+ ResolveExpr(obj, context, false, false)(false)
+ CheckNoGhost(obj, context)
+ // resolve arguments
+ args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }
+ // lookup method
+ var typ: Class = IntClass
+ obj.typ.LookupMember(id) match {
+ case None =>
+ context.Error(c.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)
+ case Some(m: Method) =>
+ c.m = m
+ if (args.length != m.ins.length)
+ context.Error(c.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +
+ " (" + args.length + " instead of " + m.ins.length + ")")
+ else {
+ for((actual, formal) <- args zip m.ins){
+ if(! canAssign(formal.t.typ, actual.typ))
+ context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")
+ }
+ }
+ case _ => context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)
+ }
+ // resolve the token
+ if (declaresLocal) {
+ // this is taken care of in the caller that handles the enclosing block statement
+ } else if (token != null) {
+ ResolveExpr(token, context, false, false)(false)
+ if(! canAssign(token.typ, TokenClass(new Type(obj.typ), id)))
+ context.Error(token.pos, "wrong token type")
+ }
+ case jn@JoinAsync(lhs, token) =>
+ // resolve the assignees
+ var vars = Set[Variable]()
+ for (v <- lhs) {
+ ResolveExpr(v, context, false, false)(false)
+ if (v.v != null) {
+ if (v.v.IsImmutable) context.Error(v.pos, "cannot use immutable variable " + v.id + " as actual out-parameter")
+ if (vars contains v.v) {
+ context.Error(v.pos, "duplicate actual out-parameter: " + v.id)
+ } else {
+ vars = vars + v.v
+ }
+ }
+ }
+ // resolve the token
+ ResolveExpr(token, context, false, false)(false);
+ if(token.typ == null || ! token.typ.IsToken || ! token.typ.isInstanceOf[TokenClass] || token.typ.asInstanceOf[TokenClass].method == null)
+ context.Error(token.pos, "the first argument of a join async must be a token")
+ else {
+ val m = token.typ.asInstanceOf[TokenClass].method;
+ jn.m = m
+ if (lhs.length != m.outs.length)
+ context.Error(jn.pos, "wrong number of actual out-parameters in join async of " + m.FullName +
+ " (" + lhs.length + " instead of " + m.outs.length + ")")
+ else {
+ for((out, l) <- m.outs zip lhs){
+ if(! canAssign(l.typ, out.t.typ))
+ context.Error(l.pos, "the out parameter cannot be assigned to the lhs (expected: " + l.typ.FullName + ", found: " + out.t.FullName + ")")
+ }
+ }
+
+ }
+ }
+
+ def ComputeLoopTargets(s: Statement): Set[Variable] = s match { // local variables
+ case BlockStmt(ss) =>
+ (ss :\ Set[Variable]()) { (s,vars) => vars ++ ComputeLoopTargets(s) }
+ case IfStmt(guard, thn, els) =>
+ val vars = ComputeLoopTargets(thn)
+ els match { case None => vars; case Some(els) => vars ++ ComputeLoopTargets(els) }
+ case w: WhileStmt =>
+ // assume w.LoopTargets is non-null and that it was computed with a larger context
+ w.LoopTargets
+ case Assign(lhs, rhs) =>
+ if (lhs.v != null) Set(lhs.v) else Set() // don't assume resolution was successful
+ case lv: LocalVar =>
+ lv.rhs match { case None => Set() case Some(_) => Set(lv.v) }
+ case Call(lhs, obj, id, args) =>
+ (lhs :\ Set[Variable]()) { (ve,vars) => if (ve.v != null) vars + ve.v else vars }
+ case _ => Set()
+ }
+
+ def ResolveAssign(lhs: VariableExpr, rhs: RValue, context: ProgramContext) = {
+ rhs match {
+ case ExplicitSeq(Nil) => rhs.typ = lhs.typ; // if [] appears on the rhs of an assignment, we "infer" its type by looking at the type of the lhs
+ case _ => ResolveExpr(rhs, context, false, false)(false)
+ }
+ if (! canAssign(lhs.typ, rhs.typ))
+ context.Error(lhs.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)
+ if (lhs.v != null && !lhs.v.IsGhost) CheckNoGhost(rhs, context)
+ }
+
+ // ResolveExpr resolves all parts of an RValue, if possible, and (always) sets the RValue's typ field
+ def ResolveExpr(e: RValue, context: ProgramContext,
+ twoStateContext: boolean, specContext: boolean)(implicit inPredicate: Boolean): unit = e match {
+ case e @ NewRhs(id, initialization) =>
+ if (context.Classes contains id) {
+ e.typ = context.Classes(id)
+ var fieldNames = Set[String]()
+ for(ini@Init(f, init) <- initialization) {
+ if (fieldNames contains f) {
+ context.Error(ini.pos, "The field " + f + " occurs more than once in initializer.")
+ } else {
+ fieldNames = fieldNames + f
+ e.typ.LookupMember(f) match {
+ case Some(field@Field(name, tp)) =>
+ if(field.isInstanceOf[SpecialField]) context.Error(init.pos, "Initializer cannot assign to special field " + name + ".");
+ ResolveExpr(init, context, false, false);
+ if(! canAssign(tp.typ, init.typ)) context.Error(init.pos, "The field " + name + " cannot be initialized with an expression of type " + init.typ.id + ".");
+ ini.f = field;
+ case _ =>
+ context.Error(e.pos, "The type " + id + " does not declare a field " + f + ".");
+ }
+ }
+ }
+ } else {
+ context.Error(e.pos, "undefined class " + id + " used in new expression")
+ e.typ = IntClass
+ }
+ case i:IntLiteral =>
+ i.typ = IntClass
+ case b:BoolLiteral =>
+ b.typ = BoolClass
+ case n:NullLiteral =>
+ n.typ = NullClass
+ case mx:MaxLockLiteral =>
+ mx.typ = MuClass
+ case mx:LockBottomLiteral =>
+ mx.typ = MuClass
+ case r:Result =>
+ assert(context.CurrentMember!=null);
+ r.typ = IntClass
+ if(context.CurrentMember==null || ! context.CurrentMember.isInstanceOf[Function]){
+ context.Error(r.pos, "The variable result can only be used in the postcondition of a function.");
+ } else {
+ r.typ = context.CurrentMember.asInstanceOf[Function].out.typ;
+ }
+ case ve @ VariableExpr(id) =>
+ context.LookupVariable(id) match {
+ case None => context.Error(ve.pos, "undefined local variable " + id); ve.typ = IntClass
+ case Some(v) => ve.v = v; ve.typ = v.t.typ }
+ case v:ThisExpr => v.typ = context.CurrentClass
+ case sel @ MemberAccess(e, id) =>
+ ResolveExpr(e, context, twoStateContext, false)
+ var typ: Class = IntClass
+ e.typ.LookupMember(id) match {
+ case None =>
+ context.Error(sel.pos, "undeclared member " + id + " in class " + e.typ.FullName)
+ case Some(f: Field) => sel.f = f; typ = f.typ.typ
+ case Some(pred@Predicate(id, body)) =>
+ if(! specContext)
+ context.Error(sel.pos, "predicate can only be used in positive predicate contexts")
+ sel.predicate = pred;
+ sel.isPredicate = true;
+ typ = BoolClass
+ case _ => context.Error(sel.pos, "field-select expression does not denote a field: " + e.typ.FullName + "." + id);
+ }
+ sel.typ = typ
+ case expr@ Access(e, perm) =>
+ if (!specContext) context.Error(expr.pos, "acc expression is allowed only in positive predicate contexts")
+ ResolveExpr(e, context, twoStateContext, true)
+ perm match {
+ case None =>
+ case Some(perm) => ResolveExpr(perm, context, twoStateContext, false) }
+ expr.typ = BoolClass
+ case expr@ RdAccess(e,perm) =>
+ if (!specContext) context.Error(expr.pos, "rd expression is allowed only in positive predicate contexts")
+ ResolveExpr(e, context, twoStateContext, true)
+ perm match {
+ case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false)
+ case _ => }
+ expr.typ = BoolClass
+ case expr@AccessAll(obj, perm) =>
+ if (!specContext) context.Error(expr.pos, "acc expression is allowed only in positive predicate contexts")
+ ResolveExpr(obj, context, twoStateContext, false)
+ if(!obj.typ.IsRef) context.Error(expr.pos, "Target of .* must be object reference.")
+ perm match {
+ case None =>
+ case Some(perm) => ResolveExpr(perm, context, twoStateContext, false) }
+ expr.typ = BoolClass
+ case expr@RdAccessAll(obj,perm) =>
+ if (!specContext) context.Error(expr.pos, "rd expression is allowed only in positive predicate contexts")
+ ResolveExpr(obj, context, twoStateContext, false)
+ if(!obj.typ.IsRef) context.Error(expr.pos, "Target of .* must be object reference.")
+ perm match {
+ case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false)
+ case _ => }
+ expr.typ = BoolClass
+ case expr@ Holds(e) =>
+ if(inPredicate) context.Error(expr.pos, "holds cannot be mentioned in monitor invariants or predicates")
+ if(! specContext)
+ context.Error(expr.pos, "holds is allowed only in positive predicate contexts");
+ //todo: check that we are not in an invariant
+ ResolveExpr(e, context, twoStateContext, false)
+ expr.typ = BoolClass
+ case expr@ RdHolds(e) =>
+ if(inPredicate) context.Error(expr.pos, "rdholds cannot be mentioned in monitor invariants or predicates")
+ ResolveExpr(e, context, twoStateContext, false)
+ expr.typ = BoolClass
+ case expr@ Assigned(id) =>
+ context.LookupVariable(id) match {
+ case None => context.Error(expr.pos, "undefined local variable " + id)
+ case Some(v) =>
+ expr.v = v
+ if (!(v.IsImmutable && v.IsGhost))
+ context.Error(expr.pos, "assigned can only be used with ghost consts")
+ }
+ expr.typ = BoolClass
+ case expr@ Old(e) =>
+ if (! twoStateContext) { context.Error(expr.pos, "old expression is not allowed here") }
+ ResolveExpr(e, context, twoStateContext, false)
+ expr.typ = e.typ
+ case ite@IfThenElse(con, then, els) =>
+ ResolveExpr(con, context, twoStateContext, false); ResolveExpr(then, context, twoStateContext, specContext); ResolveExpr(els, context, twoStateContext, specContext);
+ if (!con.typ.IsBool) context.Error(con.pos, "condition of if-then-else expression must be a boolean");
+ if (! canAssign(then.typ, els.typ)) context.Error(ite.pos, "the then and else branch of an if-then-else expression must have compatible types");
+ ite.typ = then.typ;
+ case expr@ Not(e) =>
+ ResolveExpr(e, context, twoStateContext, false)
+ if (!e.typ.IsBool) context.Error(expr.pos, "not-expression requires boolean operand")
+ expr.typ = BoolClass
+ case appl@FunctionApplication(obj, id, args) =>
+ ResolveExpr(obj, context, twoStateContext, false);
+ args foreach { arg => ResolveExpr(arg, context, twoStateContext, false)};
+ // lookup function
+ appl.typ = IntClass
+ obj.typ.LookupMember(id) match {
+ case None =>
+ context.Error(appl.pos, "function " + id + " not found in class " + obj.typ.FullName)
+ case Some(func@Function(f, ins, out, specs, body)) =>
+ appl.f = func
+ appl.typ = func.out.typ;
+ if (args.length != ins.length)
+ context.Error(appl.pos, "wrong number of actual arguments in function application of " + obj.typ.FullName + "." + id +
+ " (" + args.length + " instead of " + ins.length + ")")
+ else {
+ for((actual, formal) <- args zip func.ins){
+ if(! canAssign(formal.t.typ, actual.typ))
+ context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")
+ }
+ }
+ case _ => context.Error(appl.pos, obj.typ.id + "." + id + " is not a function")
+ }
+ case uf@Unfolding(pred, e) =>
+ ResolveExpr(pred, context, twoStateContext, true);
+ ResolveExpr(e, context, twoStateContext, false);
+ if(! pred.getMemberAccess.isPredicate) context.Error(uf.pos, "Only predicates can be unfolded.")
+ uf.typ = e.typ;
+ case bin: EqualityCompareExpr =>
+ ResolveExpr(bin.E0, context, twoStateContext, false)
+ ResolveExpr(bin.E1, context, twoStateContext, false)
+ if (bin.E0.typ == bin.E1.typ) { /* all is well */ }
+ else if (bin.E0.typ.IsRef && bin.E1.typ.IsNull) { /* all is well */ }
+ else if (bin.E0.typ.IsNull && bin.E1.typ.IsRef) { /* all is well */ }
+ else
+ context.Error(bin.pos, bin.OpName + " requires operands of the same type, found " + bin.E0.typ.FullName + " and " + bin.E1.typ.FullName)
+ bin.typ = BoolClass
+ case bin: LockBelow =>
+ ResolveExpr(bin.E0, context, twoStateContext, false)
+ ResolveExpr(bin.E1, context, twoStateContext, false)
+ if (!(bin.E0.typ.IsRef || bin.E0.typ.IsMu))
+ context.Error(bin.pos, "type of " + bin.OpName + " LHS operand must be a reference or Mu type (found " + bin.E0.typ.FullName + ")")
+ if (!(bin.E1.typ.IsRef || bin.E1.typ.IsMu))
+ context.Error(bin.pos, "type of " + bin.OpName + " RHS operand must be a reference or Mu type (found " + bin.E1.typ.FullName + ")")
+ bin.typ = BoolClass
+ case app@Append(e0, e1) =>
+ ResolveExpr(e0, context, twoStateContext, false);
+ ResolveExpr(e1, context, twoStateContext, false);
+ if(! e0.typ.IsSeq) context.Error(app.pos, "LHS operand of ++ must be sequence (found: " + e0.typ.FullName + ").");
+ if(! e1.typ.IsSeq) context.Error(app.pos, "RHS operand of ++ must be sequence (found: " + e1.typ.FullName + ").");
+ if(e0.typ != e1.typ) context.Error(app.pos, "++ can only be applied to sequences of the same type.");
+ app.typ = e0.typ;
+ case at@At(e0, e1) =>
+ ResolveExpr(e0, context, twoStateContext, false);
+ ResolveExpr(e1, context, twoStateContext, false);
+ if(! e0.typ.IsSeq) context.Error(at.pos, "LHS operand of @ must be sequence. (found: " + e0.typ.FullName + ").");
+ if(! e1.typ.IsInt) context.Error(at.pos, "RHS operand of @ must be an integer (found: " + e1.typ.FullName + ").");
+ if(e0.typ.IsSeq) at.typ = e0.typ.parameters(0) else at.typ = IntClass;
+ case drop@Drop(e0, e1) =>
+ ResolveExpr(e0, context, twoStateContext, false);
+ ResolveExpr(e1, context, twoStateContext, false);
+ if(! e0.typ.IsSeq) context.Error(drop.pos, "LHS operand of drop must be sequence. (found: " + e0.typ.FullName + ").");
+ if(! e1.typ.IsInt) context.Error(drop.pos, "RHS operand of drop must be an integer (found: " + e1.typ.FullName + ").");
+ drop.typ = e0.typ;
+ case take@Take(e0, e1) =>
+ ResolveExpr(e0, context, twoStateContext, false);
+ ResolveExpr(e1, context, twoStateContext, false);
+ if(! e0.typ.IsSeq) context.Error(take.pos, "LHS operand of take must be sequence. (found: " + e0.typ.FullName + ").");
+ if(! e1.typ.IsInt) context.Error(take.pos, "RHS operand of take must be an integer (found: " + e1.typ.FullName + ").");
+ take.typ = e0.typ;
+ case bin: BinaryExpr =>
+ ResolveExpr(bin.E0, context, twoStateContext, specContext && bin.isInstanceOf[And])
+ ResolveExpr(bin.E1, context, twoStateContext, specContext && (bin.isInstanceOf[And] || bin.isInstanceOf[Implies]))
+ if (bin.E0.typ != bin.ExpectedLhsType)
+ context.Error(bin.E0.pos, "incorrect type of " + bin.OpName + " LHS" +
+ " (expected " + bin.ExpectedLhsType.FullName +
+ ", found " + bin.E0.typ.FullName + ")")
+ if (bin.E1.typ != bin.ExpectedRhsType)
+ context.Error(bin.E1.pos, "incorrect type of " + bin.OpName + " RHS" +
+ " (expected " + bin.ExpectedRhsType.FullName + ", found " + bin.E1.typ.FullName + ")")
+ bin.typ = bin.ResultType
+ case q: Quantification =>
+ q.Is foreach { i => if(context.LookupVariable(i).isDefined) context.Error(q.pos, "The variable " + i + " hides another local.") }
+ ResolveExpr(q.Seq, context, twoStateContext, false);
+ if(! q.Seq.typ.IsSeq)
+ context.Error(q.Seq.pos, "A quantification must range over a sequence. (found: " + q.Seq.typ.FullName + ").");
+ else {
+ val elementType = q.Seq.typ.parameters(0);
+ var bodyContext = context;
+ var bvariables = Nil: List[Variable];
+ q.Is foreach { i =>
+ val variable = new Variable(i, new Type(elementType));
+ bodyContext = bodyContext.AddVariable(variable);
+ bvariables = bvariables + variable;
+ }
+ ResolveExpr(q.E, bodyContext, twoStateContext, true);
+ if(! q.E.typ.IsBool) context.Error(q.E.pos, "Body of quantification must be a boolean. (found: " + q.E.typ.FullName + ").");
+ q.variables = bvariables;
+ }
+ q.typ = BoolClass
+ case seq@EmptySeq(t) =>
+ ResolveType(t, context)
+ seq.typ = getSeqType(t.typ, context);
+ case seq@ExplicitSeq(es) =>
+ es foreach { e => ResolveExpr(e, context, twoStateContext, false) }
+ es match {
+ case Nil => seq.typ = getSeqType(IntClass, context);
+ case h :: t =>
+ t foreach { e => if(! (e.typ == h.typ)) context.Error(e.pos, "The elements of the sequence expression have different types.")};
+ seq.typ = getSeqType(h.typ, context);
+ }
+ case ran@Range(min, max) =>
+ ResolveExpr(min, context, twoStateContext, false);
+ if(! min.typ.IsInt) context.Error(min.pos, "The mininum of a range expression must be an integer (found: " + min.typ.FullName + ").");
+ ResolveExpr(max, context, twoStateContext, false);
+ if(! max.typ.IsInt) context.Error(max.pos, "The maximum of a range expression must be an integer (found: " + max.typ.FullName + ").");
+ ran.typ = getSeqType(IntClass, context);
+ case len@Length(e) =>
+ ResolveExpr(e, context, twoStateContext, false);
+ if(! e.typ.IsSeq) context.Error(len.pos, "The operand of a length expression must be sequence. (found: " + e.typ.FullName + ").");
+ len.typ = IntClass;
+ case ev@Eval(h, e) =>
+ if(inPredicate) context.Error(ev.pos, "eval cannot be used in monitor invariants or predicates")
+ h match {
+ case AcquireState(obj) =>
+ ResolveExpr(obj, context, twoStateContext, false)
+ if(! obj.typ.IsRef) context.Error(ev.pos, "The target of acquire must be a reference.");
+ case ReleaseState(obj) => ResolveExpr(obj, context, twoStateContext, false)
+ if(! obj.typ.IsRef) context.Error(ev.pos, "The target of acquire must be a reference.");
+ case c@CallState(token, obj, id, args) =>
+ ResolveExpr(token, context, twoStateContext, false);
+ if( ! token.typ.IsToken) context.Error(token.pos, "joinable is only applicable to tokens");
+ ResolveExpr(obj, context, false, false)
+ CheckNoGhost(obj, context)
+ args foreach { a => ResolveExpr(a, context, false, false); CheckNoGhost(a, context) }
+ // lookup method
+ var typ: Class = IntClass
+ obj.typ.LookupMember(id) match {
+ case None =>
+ context.Error(obj.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)
+ case Some(m: Method) =>
+ c.m = m
+ if (args.length != m.ins.length)
+ context.Error(obj.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +
+ " (" + args.length + " instead of " + m.ins.length + ")")
+ else {
+ for((actual, formal) <- args zip m.ins){
+ if(! canAssign(formal.t.typ, actual.typ))
+ context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")
+ }
+ }
+ case _ => context.Error(obj.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)
+ }
+
+
+ }
+ ResolveExpr(e, context, false, specContext)
+ ev.typ = e.typ;
+ }
+
+ def LookupRunMethod(cl: Class, context: ProgramContext, op: String, pos: Position): Option[Method] = {
+ cl.LookupMember("run") match {
+ case None =>
+ context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +
+ " (found type " + cl.id + ")")
+ None
+ case Some(m: Method) =>
+ m.spec foreach {
+ case Precondition(e) => CheckRunSpecification(e, context, true)
+ case Postcondition(e) => CheckRunSpecification(e, context, false)
+ case lc: LockChange => context.Error(lc.pos, "lockchange is not allowed in specification of run method")
+ }
+ if(0<m.ins.length || 0<m.outs.length) {
+ context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +
+ " (found " + m.ins.length + " in-parameters and " + m.outs.length + " out-parameters)"); None
+ } else
+ Some(m)
+ case _ =>
+ context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +
+ " (found non-method member)")
+ None
+ }
+ }
+
+ // assumes that lhs and rhs are resolved
+ def canAssign(lhs: Class, rhs: Class): Boolean = {
+ (lhs, rhs) match {
+ case (TokenClass(c1, m1), TokenClass(c2, m2)) => c1.id.equals(c2.id) && m1.equals(m2)
+ case (TokenClass(c1, m1), _) => false
+ case (_, TokenClass(c2, m2)) => false
+ case (lhs, rhs) => lhs == rhs || (lhs.IsRef && rhs.IsNull)
+ }
+ }
+
+ def CheckNoGhost(expr: RValue, context: ProgramContext): Unit = {
+ def specOk(e: RValue): Unit = {
+ e match {
+ case ve: VariableExpr =>
+ if (ve.v != null && ve.v.IsGhost) context.Error(ve.pos, "ghost variable not allowed here")
+ case fs@ MemberAccess(e, id) =>
+ if (!fs.isPredicate && fs.f != null && fs.f.IsGhost) context.Error(fs.pos, "ghost fields not allowed here")
+ CheckNoGhost(e, context)
+ case a: Assigned =>
+ if (a.v != null && a.v.IsGhost) context.Error(a.pos, "ghost variable not allowed here")
+ case _ => visitE(e, specOk)
+ }
+ }
+ specOk(expr)
+ }
+
+ def CheckNoImmutableGhosts(expr: RValue, context: ProgramContext): Unit = {
+ def specOk(e: RValue): Unit = {
+ e match {
+ case ve: VariableExpr =>
+ if (ve.v != null && ve.v.IsGhost && ve.v.IsImmutable) context.Error(ve.pos, "ghost const not allowed here")
+ case a: Assigned =>
+ if (a.v != null && a.v.IsGhost && a.v.IsImmutable) context.Error(a.pos, "ghost const not allowed here")
+ case _ => visitE(e, specOk)
+ }
+ }
+ specOk(expr)
+ }
+
+ def CheckRunSpecification(e: Expression, context: ProgramContext, allowMaxLock: boolean): unit = e match {
+ case _:MaxLockLiteral =>
+ if (!allowMaxLock) context.Error(e.pos, "specification of run method is not allowed to mention maxlock here")
+ case _:Literal =>
+ case _:VariableExpr =>
+ case _:ThisExpr =>
+ case _:Result =>
+ case MemberAccess(e, id) =>
+ CheckRunSpecification(e, context, false)
+ case Access(e, perm) =>
+ CheckRunSpecification(e, context, false)
+ perm match { case None => case Some(perm) => CheckRunSpecification(perm, context, false) }
+ case RdAccess(e, perm) =>
+ CheckRunSpecification(e, context, false)
+ perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => }
+ case AccessAll(obj, perm) =>
+ CheckRunSpecification(obj, context, false)
+ perm match { case None => case Some(perm) => CheckRunSpecification(perm, context, false) }
+ case RdAccessAll(obj, perm) =>
+ CheckRunSpecification(obj, context, false)
+ perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => }
+ case Holds(e) =>
+ context.Error(e.pos, "holds is not allowed in specification of run method")
+ case RdHolds(e) =>
+ context.Error(e.pos, "rd holds is not allowed in specification of run method")
+ case _:Assigned =>
+ case Old(e) =>
+ CheckRunSpecification(e, context, false) // OLD occurs only in postconditions and monitor invariants, where maxlock is not allowed anyhow
+ case IfThenElse(con, then, els) =>
+ CheckRunSpecification(con, context, false);
+ CheckRunSpecification(con, context, allowMaxLock);
+ CheckRunSpecification(con, context, allowMaxLock);
+ case Not(e) =>
+ CheckRunSpecification(e, context, false)
+ case FunctionApplication(obj, id, args) =>
+ obj :: args foreach { arg => CheckRunSpecification(arg, context, false)}
+ case Unfolding(pred, e) =>
+ CheckRunSpecification(pred, context, true);
+ CheckRunSpecification(e, context, allowMaxLock);
+ case LockBelow(e0,e1) =>
+ CheckRunSpecification(e0, context, allowMaxLock)
+ CheckRunSpecification(e1, context, false)
+ case And(e0,e1) =>
+ CheckRunSpecification(e0, context, allowMaxLock)
+ CheckRunSpecification(e1, context, allowMaxLock)
+ case Implies(e0,e1) =>
+ CheckRunSpecification(e0, context, false)
+ CheckRunSpecification(e1, context, allowMaxLock)
+ case bin: BinaryExpr =>
+ CheckRunSpecification(bin.E0, context, false)
+ CheckRunSpecification(bin.E1, context, false)
+ case q: Quantification =>
+ CheckRunSpecification(q.Seq, context, false)
+ CheckRunSpecification(q.E, context, true)
+ case Length(e) =>
+ CheckRunSpecification(e, context, false);
+ case ExplicitSeq(es) =>
+ es foreach { e => CheckRunSpecification(e, context, false) }
+ case Range(min, max) =>
+ CheckRunSpecification(min, context, false)
+ CheckRunSpecification(max, context, false)
+ case Eval(h, e) =>
+ h match {
+ case AcquireState(obj) => CheckRunSpecification(obj, context, false);
+ case ReleaseState(obj) => CheckRunSpecification(obj, context, false);
+ case CallState(token, obj, id, args) => CheckRunSpecification(token, context, false); CheckRunSpecification(obj, context, false); args foreach { a: Expression => CheckRunSpecification(a, context, false)};
+ }
+ CheckRunSpecification(e, context, allowMaxLock)
+ }
+
+ def visitE(expr: RValue, func: RValue => Unit): Unit = {
+ expr match {
+ case _:NewRhs =>
+ case e: Literal => ;
+ case _:ThisExpr => ;
+ case _:Result => ;
+ case e:VariableExpr => ;
+ case acc@MemberAccess(e,f) =>
+ func(e);
+ case Access(e, perm) =>
+ func(e); perm match { case Some(p) => func(p); case _ => ; }
+ case RdAccess(e, perm) =>
+ func(e); perm match { case Some(Some(p)) => func(p); case _ => ; }
+ case AccessAll(obj, perm) =>
+ 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 Holds(e) => func(e);
+ case RdHolds(e) => func(e);
+ case e: Assigned => e
+ case Old(e) => func(e);
+ case IfThenElse(con, then, els) => func(con); func(then); func(els);
+ case Not(e) => func(e);
+ case funapp@FunctionApplication(obj, id, args) =>
+ func(obj); args foreach { arg => func(arg) };
+ case Unfolding(pred, e) =>
+ func(pred); func(e);
+ case Iff(e0,e1) => func(e0); func(e1);
+ case Implies(e0,e1) => func(e0); func(e1);
+ case And(e0,e1) =>func(e0); func(e1);
+ case Or(e0,e1) => func(e0); func(e1);
+ case Eq(e0,e1) => func(e0); func(e1);
+ case Neq(e0,e1) => func(e0); func(e1);
+ case Less(e0,e1) => func(e0); func(e1);
+ case AtMost(e0,e1) => func(e0); func(e1);
+ case AtLeast(e0,e1) => func(e0); func(e1);
+ case Greater(e0,e1) => func(e0); func(e1);
+ case LockBelow(e0,e1) => func(e0); func(e1);
+ case Plus(e0,e1) => func(e0); func(e1);
+ case Minus(e0,e1) => func(e0); func(e1);
+ case Times(e0,e1) => func(e0); func(e1);
+ 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 ExplicitSeq(es) =>
+ es foreach { e => func(e) }
+ case Range(min, max) =>
+ func(min); func(max);
+ case Append(e0, e1) =>
+ func(e0); func(e1);
+ case at@At(e0, e1) =>
+ func(e0); func(e1);
+ case Drop(e0, e1) =>
+ func(e0); func(e1);
+ case Take(e0, e1) =>
+ func(e0); func(e1);
+ case Length(e) =>
+ func(e)
+ case Eval(h, e) =>
+ h match {
+ case AcquireState(obj) => func(obj);
+ case ReleaseState(obj) => func(obj);
+ case CallState(token, obj, id, args) => func(token); func(obj); args foreach {a : Expression => func(a)};
+ }
+ func(e);
+ }
+ }
+}
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala new file mode 100644 index 00000000..9ec41448 --- /dev/null +++ b/Chalice/src/Translator.scala @@ -0,0 +1,2260 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+import scala.util.parsing.input.Position
+
+import Boogie.Proc, Boogie.NamedType, Boogie.NewBVar, Boogie.Havoc, Boogie.Stmt, Boogie.Const,
+ Boogie.Decl, Boogie.Expr, Boogie.FunctionApp, Boogie.Axiom, Boogie.BVar, Boogie.BType,
+ Boogie.VarExpr, Boogie.IndexedType, Boogie.Comment, Boogie.MapUpdate, Boogie.MapSelect,
+ Boogie.If;
+
+case class ErrorMessage(pos: Position, message: String)
+
+object TranslationOptions {
+ // note: the initial values should match those Chalice.scala
+
+ var defaults = 0: int;
+ var autoFold = false: Boolean;
+ var checkLeaks = false: Boolean;
+ var autoMagic = false: Boolean;
+}
+
+class Translator {
+ import TranslationHelper._;
+ import TranslationOptions._;
+ var currentClass = null: Class;
+ var currentMethod = null: Method;
+ var modules = Nil: List[String]
+ var etran = new ExpressionTranslator(null);
+
+ def translateProgram(classes: List[Class]): List[Decl] = {
+ classes flatMap { translateClass(_) }
+ }
+
+ def translateClass(cl: Class): List[Decl] = {
+ currentClass = cl;
+ etran = new ExpressionTranslator(cl);
+ var declarations = Nil: List[Decl]
+ // add module (if no added yet)
+ if(modules forall {mname => ! mname.equals(cl.module)}) {
+ declarations = declarations + Const(ModuleName(cl), true, ModuleType);
+ modules = modules + cl.module;
+ }
+ // add class name
+ declarations = declarations + Const(cl.id + "#t", true, TypeName);
+ // translate monitor invariant
+ declarations = declarations ::: translateMonitorInvariant(cl.Invariants);
+ // translate each member
+ for(member <- cl.members) {
+ declarations = declarations ::: translateMember(member);
+ }
+ declarations
+ }
+
+ /**********************************************************************
+ ***************** MEMBERS *****************
+ **********************************************************************/
+
+ def translateMember(member: Member): List[Decl] = {
+ member match {
+ case f: Field =>
+ translateField(f)
+ case m: Method =>
+ translateMethod(m)
+ case f: Function =>
+ translateFunction(f)
+ case pred: Predicate =>
+ translatePredicate(pred)
+ case inv: MonitorInvariant =>
+ Nil // already dealt with before
+ }
+ }
+
+ def translateMonitorInvariant(invs: List[MonitorInvariant]): List[Decl] = {
+ val (m1V, m1) = NewBVar("m1", tmask, true); val (h1V, h1) = NewBVar("h1", theap, true);
+ val (m2V, m2) = NewBVar("m2", tmask, true); val (h2V, h2) = NewBVar("h2", theap, true);
+ val (lkV, lk) = NewBVar("lk", tref, true);
+ val oldTranslator = new ExpressionTranslator(List(h2, m2), List(h1, m1), currentClass);
+ Proc(currentClass.id + "$monitorinvariant$checkDefinedness",
+ List(NewBVarWhere("this", new Type(currentClass))),
+ Nil,
+ GlobalNames,
+ DefaultPrecondition(),
+ BLocal(h1V) :: BLocal(m1V) ::BLocal(h2V) :: BLocal(m2V) :: BLocal(lkV) ::
+ bassume(wf(h1, m1)) :: bassume(wf(h2, m2)) ::
+ (oldTranslator.Mask := ZeroMask) ::
+ oldTranslator.Inhale(invs map { mi => mi.e}, "monitor invariant", false) :::
+ (etran.Mask := ZeroMask) ::
+ Havoc(etran.Heap) ::
+ // check that invariant is well-defined
+ etran.WhereOldIs(h2, m2).Inhale(invs map { mi => mi.e}, "monitor invariant", true) :::
+ (if (!checkLeaks || invs.length == 0) Nil else
+ // check that there are no loops among .mu permissions in monitors
+ // !CanWrite[this,mu]
+ bassert(!etran.CanWrite(VarExpr("this"), "mu"), invs(0).pos, "Monitor invariant is not allowed to hold write permission to this.mu") ::
+ // (forall lk :: lk != null && lk != this && CanRead[lk,mu] ==>
+ // CanRead[this,mu] && Heap[this,mu] << Heap[lk,mu])
+ bassert(
+ (lk !=@ NullLiteral() && lk !=@ VarExpr("this") && etran.CanRead(lk, "mu")) ==>
+ (etran.CanRead(VarExpr("this"), "mu") &&
+ new FunctionApp("MuBelow", etran.Heap.select(VarExpr("this"), "mu"), etran.Heap.select(lk, "mu"))),
+ invs(0).pos,
+ "Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu")
+ ) :::
+ //check that invariant is reflexive
+ etran.UseCurrentAsOld().Exhale(invs map {mi => (mi.e, ErrorMessage(mi.pos, "Monitor invariant might not be reflexive."))}, "invariant reflexive?", false))
+ }
+
+ def translateField(f: Field): List[Decl] = {
+ Const(f.FullName, true, FieldType(f.typ)) ::
+ Axiom(NonPredicateField(f.FullName))
+ }
+
+ def translateFunction(f: Function): List[Decl] = {
+ val myresult = BVar("result", Boogie.ClassType(f.out.typ));
+ etran.checkTermination = true;
+ val checkBody = isDefined(f.definition);
+ etran.checkTermination = false;
+ // BoogiePL function that represents the dafny function
+ Boogie.Function(functionName(f), BVar("heap", theap) :: Boogie.BVar("mask", tmask) :: Boogie.BVar("this", tref) :: (f.ins map Variable2BVar), new Boogie.BVar("$myresult", Boogie.ClassType(f.out.typ))) ::
+ // check definedness of the function's precondition and body
+ Proc(f.FullName + "$checkDefinedness",
+ NewBVarWhere("this", new Type(currentClass)) :: (f.ins map {i => Variable2BVarWhere(i)}),
+ Nil,
+ GlobalNames,
+ DefaultPrecondition(),
+ DefinePreInitialState :::
+ // check definedness of the precondition
+ InhaleWithChecking(Preconditions(f.spec) map { p => (if(0<defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition") :::
+ bassume(CurrentModule ==@ VarExpr(ModuleName(currentClass))) :: // verify the body assuming that you are in the module
+ // check definedness of function body
+ checkBody :::
+ BLocal(myresult) ::
+ (Boogie.VarExpr("result") := etran.Tr(f.definition)) ::
+ // check that postcondition holds
+ ExhaleWithChecking(Postconditions(f.spec) map { post => ((if(0<defaults) UnfoldPredicatesWithReceiverThis(post) else post), ErrorMessage(f.pos, "Postcondition at " + post.pos + " might not hold."))}, "function postcondition")) ::
+ // definition axiom
+ definitionAxiom(f) ::
+ // framing axiom (+ frame function)
+ framingAxiom(f) :::
+ // postcondition axiom(s)
+ postconditionAxiom(f)
+ }
+
+ def definitionAxiom(f: Function): Axiom = {
+ val version = Version(Preconditions(f.spec).foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b) }), etran);
+ val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
+ val frameFunctionName = "##" + f.FullName;
+
+ /* axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::
+ wf(h, m) && CurrentModule == module#C ==> #C.f(h, m, this, x_1, ..., x_n) == tr(body))
+ */
+ val args = VarExpr("this") :: inArgs;
+ val applyF = f.apply(List(etran.Heap, etran.Mask) ::: args);
+ Axiom(new Boogie.Forall(
+ BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),
+ List(applyF),
+ (wf(Heap, Mask) && (CurrentModule ==@ ModuleName(currentClass)))
+ ==>
+ (applyF ==@ etran.Tr(f.definition)))
+ )
+ }
+
+ def framingAxiom(f: Function): List[Decl] = {
+ /* function ##C.f(state, ref, t_1, ..., t_n) returns (t);
+ axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::
+ wf(h, m) && IsGoodState(version) ==> #C.f(h, m, this, x_1, ..., x_n) == ##C.f(version, this, x_1, ..., x_n))
+ */
+ val version = Version(Preconditions(f.spec).foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b) }), etran);
+ val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
+ val frameFunctionName = "##" + f.FullName;
+
+ val args = VarExpr("this") :: inArgs;
+ val applyF = f.apply(List(etran.Heap, etran.Mask) ::: args);
+ val applyFrameFunction = FunctionApp(frameFunctionName, version :: args);
+ Boogie.Function("##" + f.FullName, Boogie.BVar("state", theap) :: Boogie.BVar("this", tref) :: (f.ins map Variable2BVar), new BVar("$myresult", f.out)) ::
+ Axiom(new Boogie.Forall(
+ BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),
+ List(applyF),
+ (wf(Heap, Mask) && IsGoodState(version) && CanAssumeFunctionDefs)
+ ==>
+ (applyF ==@ applyFrameFunction))
+ )
+ }
+
+ def postconditionAxiom(f: Function): List[Decl] = {
+ /* function ##C.f(state, ref, t_1, ..., t_n) returns (t);
+ axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::
+ wf(h, m) && CanAssumeFunctionDefs ==> Q[#C.f(h, m, this, x_1, ..., x_n)/result]
+ */
+ val version = Version(Preconditions(f.spec).foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b) }), etran);
+ val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
+ val myresult = Boogie.BVar("result", Boogie.ClassType(f.out.typ));
+ val args = VarExpr("this") :: inArgs;
+ val applyF = f.apply(List(Heap, Mask) ::: args)
+ //postcondition axioms
+ (Postconditions(f.spec) map { post : Expression =>
+ Axiom(new Boogie.Forall(
+ BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),
+ List(applyF),
+ (wf(Heap, Mask) && CanAssumeFunctionDefs)
+ ==>
+ etran.Tr(SubstResult(post, f.apply(ExplicitThisExpr(), f.ins map { arg => new VariableExpr(arg) })))
+ ))
+ })
+ }
+
+ def translatePredicate(pred: Predicate): List[Decl] = {
+ // const unique class.name: HeapType;
+ Const(pred.FullName, true, FieldType(theap)) ::
+ // axiom PredicateField(f);
+ Axiom(PredicateField(pred.FullName)) ::
+ // check definedness of predicate body
+ Proc(pred.FullName + "$checkDefinedness",
+ List(NewBVarWhere("this", new Type(currentClass))),
+ Nil,
+ GlobalNames,
+ DefaultPrecondition(),
+ DefinePreInitialState :::
+ InhaleWithChecking(List(DefinitionOf(pred)), "predicate definition"))
+ }
+
+ def translateMethod(method: Method): List[Decl] = {
+ // check definedness of the method contract
+ Proc(method.FullName + "$checkDefinedness",
+ NewBVarWhere("this", new Type(currentClass)) :: (method.ins map {i => Variable2BVarWhere(i)}),
+ method.outs map {i => Variable2BVarWhere(i)},
+ GlobalNames,
+ DefaultPrecondition(),
+ DefinePreInitialState :::
+ bassume(CanAssumeFunctionDefs) ::
+ // check precondition
+ InhaleWithChecking(Preconditions(method.spec), "precondition") :::
+ DefineInitialState :::
+ (Mask := ZeroMask) ::
+ Havoc(etran.Heap) ::
+ // check postcondition
+ InhaleWithChecking(Postconditions(method.spec), "postcondition") :::
+ // check lockchange
+ (LockChanges(method.spec) flatMap { lc => isDefined(lc)})) ::
+ // check that method body satisfies the method contract
+ Proc(method.FullName,
+ NewBVarWhere("this", new Type(currentClass)) :: (method.ins map {i => Variable2BVarWhere(i)}),
+ method.outs map {i => Variable2BVarWhere(i)},
+ GlobalNames,
+ DefaultPrecondition(),
+ bassume(CurrentModule ==@ Boogie.VarExpr(ModuleName(currentClass))) ::
+ bassume(CanAssumeFunctionDefs) ::
+ DefinePreInitialState :::
+ Inhale(Preconditions(method.spec) map { p => (if(0<defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition") :::
+ DefineInitialState :::
+ translateStatements(method.body) :::
+ Exhale(Postconditions(method.spec) map { p => ((if(0<defaults) UnfoldPredicatesWithReceiverThis(p) else p), ErrorMessage(method.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition") :::
+ (if(checkLeaks) isLeaking(method.pos, "Method " + method.FullName + " might leak refereces.") else Nil) :::
+ bassert(LockFrame(LockChanges(method.spec), etran), method.pos, "Method might lock/unlock more than allowed.")) :: Nil
+ }
+
+ def DefaultPrecondition() : List[String] =
+ {
+ List("requires this!=null;", "free requires wf(Heap, Mask);")
+ }
+ def DefinePreInitialState = {
+ Comment("define pre-initial state") ::
+ (etran.Mask := ZeroMask)
+ }
+ def DefineInitialState = {
+ Comment("define initial state") ::
+ bassume(etran.Heap ==@ Boogie.Old(etran.Heap)) ::
+ bassume(etran.Mask ==@ Boogie.Old(etran.Mask))
+ }
+
+ /**********************************************************************
+ ***************** STATEMENTS *****************
+ **********************************************************************/
+ def translateStatements(statements: List[Statement]): List[Stmt] = {
+ statements flatMap translateStatement
+ }
+
+ def translateStatement(s: Statement): List[Stmt] = {
+ s match {
+ case Assert(e) =>
+ val newGlobals = etran.FreshGlobals("assert");
+ val tmpHeap = Boogie.NewBVar(HeapName, theap, true);
+ val tmpMask = Boogie.NewBVar(MaskName, tmask, true);
+ val tmpTranslator = new ExpressionTranslator(List(tmpHeap._1.id, tmpMask._1.id), currentClass);
+ Comment("assert") ::
+ // exhale e in a copy of the heap/mask
+ BLocal(tmpHeap._1) :: (tmpHeap._2 := Heap) ::
+ BLocal(tmpMask._1) :: (tmpMask._2 := Mask) ::
+ tmpTranslator.Exhale(List((e, ErrorMessage(s.pos, "Assertion might not hold."))), "assert", true)
+ case Assume(e) =>
+ Comment("assume") ::
+ isDefined(e) :::
+ bassume(e)
+ case BlockStmt(ss) =>
+ translateStatements(ss)
+ case IfStmt(guard, then, els) =>
+ val tt = translateStatement(then)
+ val et = els match {
+ case None => Nil
+ case Some(els) => translateStatement(els) }
+ Comment("if") ::
+ isDefined(guard) :::
+ Boogie.If(guard, tt, et)
+ case w: WhileStmt =>
+ translateWhile(w)
+ case Assign(lhs, rhs) =>
+ def assignOrAssumeEqual(r: Boogie.Expr): List[Boogie.Stmt] = {
+ if (lhs.v.isInstanceOf[ImmutableVariable]) {
+ // this must be a "ghost const"
+ val name = lhs.v.UniqueName
+ bassert(! VarExpr("assigned$" + name), lhs.pos, "Const variable can be assigned to only once.") ::
+ bassume(lhs ==@ r) ::
+ (VarExpr("assigned$" + name) := true)
+ } else {
+ lhs := r
+ }
+ }
+ Comment("assigment to " + lhs.id) ::
+ (rhs match {
+ case rhs@NewRhs(c, initialization) => // x := new C;
+ val (nw, ss) = translateAllocation(rhs.typ, initialization);
+ ss ::: assignOrAssumeEqual(new VarExpr(nw))
+ case rhs: Expression => // x := E;
+ isDefined(rhs) ::: assignOrAssumeEqual(rhs)
+ })
+ case FieldUpdate(lhs@MemberAccess(target, f), rhs) =>
+ val (statements, toStore : Expr) =
+ (rhs match {
+ case rhs @ NewRhs(c, initialization) =>
+ // e.f := new C;
+ val (nw,ss) = translateAllocation(rhs.typ, initialization)
+ (ss, new VarExpr(nw))
+ case rhs : Expression =>
+ // e.f := E;
+ (isDefined(rhs), TrExpr(rhs))
+ });
+ Comment("update field " + f) ::
+ isDefined(target) :::
+ bassert(CanWrite(target, lhs.f), s.pos, "Location might not be writable") ::
+ statements ::: etran.Heap.store(target, lhs.f, toStore) :: bassume(wf(Heap, Mask))
+ case lv @ LocalVar(id, t, const, ghost, rhs) =>
+ val bv = Variable2BVarWhere(lv.v)
+ val isAssignedVar = if (const) new Boogie.BVar("assigned$" + bv.id, Boogie.ClassType(BoolClass)) else null
+ Comment("local " + (if (ghost) "ghost " else "") + (if (const) "const " else "var ") + id) ::
+ BLocal(bv) ::
+ { if (const)
+ // havoc x; var assigned$x: bool; assigned$x := false;
+ Havoc(new Boogie.VarExpr(bv)) ::
+ BLocal(isAssignedVar) :: (new Boogie.VarExpr(isAssignedVar) := false)
+ else
+ List() } :::
+ { rhs match {
+ //update the local, provided a rhs was provided
+ case None => List()
+ case Some(rhs) => translateStatement(Assign(new VariableExpr(lv.v), rhs)) }}
+ case c: Call =>
+ translateCall(c)
+ case Install(obj, lowerBounds, upperBounds) =>
+ Comment("install") ::
+ isDefined(obj) :::
+ bassert(nonNull(obj), s.pos, "The target of the install statement might be null.") ::
+ bassert(isHeld(obj), s.pos, "The lock of the target of the install statement might not be held.") ::
+ // assert CanWrite(obj.mu); assume lowerbounds < obj.mu < upperBounds;
+ UpdateMu(obj, false, lowerBounds, upperBounds, ErrorMessage(s.pos, "Install might fail."))
+ case Share(obj, lowerBounds, upperBounds) =>
+ val (preShareMaskV, preShareMask) = Boogie.NewBVar("preShareMask", tmask, true)
+ Comment("share") ::
+ // remember the mask immediately before the share
+ BLocal(preShareMaskV) :: Boogie.Assign(preShareMask, etran.Mask) ::
+ isDefined(obj) :::
+ bassert(nonNull(obj), s.pos, "The target of the share statement might be null.") ::
+ UpdateMu(obj, true, lowerBounds, upperBounds, ErrorMessage(s.pos, "Share might fail.")) :::
+ bassume(!isHeld(obj) && ! isRdHeld(obj)) :: // follows from o.mu==lockbottom
+ // no permission to o.held
+ etran.SetNoPermission(etran.Tr(obj), "held", etran.Mask) ::
+ // exhale the monitor invariant (using the current state as the old state)
+ ExhaleInvariants(obj, false, ErrorMessage(s.pos, "Monitor invariant might not hold."), etran.UseCurrentAsOld()) :::
+ // assume a seen state is the one right before the share
+ bassume(LastSeenHeap(etran.Heap.select(obj, "mu"), etran.Heap.select(obj, "held")) ==@ etran.Heap) ::
+ bassume(LastSeenMask(etran.Heap.select(obj, "mu"), etran.Heap.select(obj, "held")) ==@ preShareMask)
+ case Unshare(obj) =>
+ val (heldV, held) = Boogie.NewBVar("held", Boogie.NamedType("int"), true)
+ val o = TrExpr(obj)
+ Comment("unshare") ::
+ isDefined(obj) :::
+ bassert(nonNull(o), s.pos, "The target of the unshare statement might be null.") ::
+ bassert(CanWrite(o, "mu"), s.pos, "The mu field of the target of the unshare statement might not be writable.") ::
+ bassert(CanWrite(o, "held"), s.pos, "The held field of the target of the unshare statement might not be writable.") ::
+ bassert(isShared(o), s.pos, "The target of the unshare statement might not be shared.") ::
+ bassert(isHeld(o), s.pos, "The target of the unshare statement might not be locked by the current thread.") :: // locked or read-locked
+ etran.Heap.store(o, "mu", bLockBottom) ::
+ // havoc o.held where 0<=o.held
+ BLocal(heldV) :: Boogie.Havoc(held) :: bassume(held <= 0) ::
+ etran.Heap.store(o, "held", held) ::
+ // set the permission of o.held to 0
+ etran.SetNoPermission(o, "held", etran.Mask) ::
+ // set o.rdheld to false
+ etran.Heap.store(o, "rdheld", false)
+ case Acquire(obj) =>
+ Comment("acquire") ::
+ isDefined(obj) :::
+ bassert(nonNull(TrExpr(obj)), s.pos, "The target of the acquire statement might be null.") ::
+ TrAcquire(s, obj)
+ case Release(obj) =>
+ Comment("release") ::
+ isDefined(obj) :::
+ bassert(nonNull(TrExpr(obj)), s.pos, "The target of the release statement might be null.") ::
+ TrRelease(s, obj)
+ case Lock(e, body, readonly) =>
+ val objV = new Variable("lock", new Type(e.typ))
+ val obj = new VariableExpr(objV)
+ val sname = if (readonly) "rd lock" else "lock"
+ val o = TrExpr(obj)
+ Comment(sname) ::
+ isDefined(e) :::
+ BLocal(Variable2BVar(objV)) :: (o := TrExpr(e)) ::
+ bassert(nonNull(o), s.pos, "The target of the " + sname + " statement might be null.") ::
+ { if (readonly) {
+ TrRdAcquire(s, obj) :::
+ translateStatement(body) :::
+ TrRdRelease(s, obj)
+ } else {
+ TrAcquire(s, obj) :::
+ translateStatement(body) :::
+ TrRelease(s, obj)
+ }
+ }
+ case RdAcquire(obj) =>
+ Comment("rd acquire") ::
+ isDefined(obj) :::
+ bassert(nonNull(TrExpr(obj)), s.pos, "The target of the read-acquire statement might be null.") ::
+ TrRdAcquire(s, obj)
+ case rdrelease@RdRelease(obj) =>
+ Comment("rd release") ::
+ isDefined(obj) :::
+ bassert(nonNull(TrExpr(obj)), obj.pos, "The target of the read-release statement might be null.") ::
+ TrRdRelease(s, obj)
+ case downgrade@Downgrade(obj) =>
+ val o = TrExpr(obj);
+ val prevHeapV = new Boogie.BVar("prevHeap", theap, true)
+ Comment("downgrade") ::
+ isDefined(obj) :::
+ bassert(nonNull(o), s.pos, "The target of the downgrade statement might be null.") ::
+ bassert(isHeld(o), s.pos, "The lock of the target of the downgrade statement might not be held by the current thread.") ::
+ bassert(! isRdHeld(o), s.pos, "The current thread might hold the read lock.") ::
+ ExhaleInvariants(obj, false, ErrorMessage(downgrade.pos, "Monitor invariant might not hold.")) :::
+ BLocal(prevHeapV) ::
+ InhaleInvariants(obj, true) :::
+ bassume(etran.Heap ==@ new Boogie.VarExpr(prevHeapV)) ::
+ etran.Heap.store(o, "rdheld", true)
+ case Free(obj) =>
+ val o = TrExpr(obj);
+ isDefined(obj) :::
+ bassert(nonNull(o), s.pos, "The target of the free statement might be null.") ::
+ (for (f <- obj.typ.Fields ++ RootClass.MentionableFields) yield
+ bassert(CanWrite(o, f.FullName), s.pos, "The field " + f.id + " of the target of the free statement might not be writable.")) :::
+ (for (f <- obj.typ.Fields ++ RootClass.MentionableFields) yield
+ etran.SetNoPermission(o, f.FullName, etran.Mask))
+ // probably need to havoc all the fields! Do we check enough?
+ case fold@Fold(acc@Access(pred@MemberAccess(e, f), fraction)) =>
+ val o = TrExpr(e);
+ var definition = if(fraction.isDefined) FractionOf(SubstThis(DefinitionOf(pred.predicate), e), fraction.get) else SubstThis(DefinitionOf(pred.predicate), e);
+ Comment("fold") ::
+ isDefined(e) :::
+ bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
+ (if(fraction.isDefined) isDefined(fraction.get) :::
+ bassert(0 <= etran.Tr(fraction.get), s.pos, "Fraction might be negative.") ::
+ bassert(etran.Tr(fraction.get) <= 100, s.pos, "Fraction might be larger than 100.") :: Nil else Nil) :::
+ // remove the definition from the current state, and replace by predicate itself
+ Exhale(List((definition, ErrorMessage(s.pos, "Fold might fail because the definition of " + pred.predicate.FullName + " does not hold."))), "fold") :::
+ Inhale(List(acc), "fold") :::
+ etran.Heap.store(o, pred.predicate.FullName, etran.Heap) :: // Is this necessary?
+ bassume(wf(etran.Heap, etran.Mask))
+ case fld@Fold(acc@RdAccess(pred@MemberAccess(e, f), nbEpsilons)) =>
+ val o = TrExpr(e);
+ var (definition, checkEpsilons) = nbEpsilons match {
+ case None => (EpsilonsOf(SubstThis(pred.predicate.definition, e), IntLiteral(1)), Nil)
+ case Some(None) => throw new Exception("Not supported yet!");
+ case Some(Some(i)) => (EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), e), i), isDefined(i) ::: bassert(Boogie.IntLiteral(0) <= i, s.pos, "Number of epsilons might be negative.") :: Nil)
+ }
+ Comment("fold") ::
+ isDefined(e) :::
+ bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
+ checkEpsilons :::
+ Exhale(List((definition, ErrorMessage(fld.pos, "Fold might fail because the definition of " + pred.predicate.FullName + " does not hold."))), "fold") :::
+ Inhale(List(acc), "fold") :::
+ etran.Heap.store(e, pred.predicate.FullName, etran.Heap) ::
+ bassume(wf(etran.Heap, etran.Mask))
+ case unfld@Unfold(acc@Access(pred@MemberAccess(e, f), fraction)) =>
+ val o = TrExpr(e);
+ var definition = if(fraction.isDefined) FractionOf(SubstThis(DefinitionOf(pred.predicate), e), fraction.get) else SubstThis(DefinitionOf(pred.predicate), e);
+ Comment("unfold") ::
+ isDefined(e) :::
+ bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
+ (if(fraction.isDefined) isDefined(fraction.get) :::
+ bassert(Boogie.IntLiteral(0) <= fraction.get, s.pos, "Fraction might be negative.") ::
+ bassert(fraction.get <= 100, s.pos, "Fraction might be larger than 100.") :: Nil else Nil) :::
+ Exhale(List((acc, ErrorMessage(s.pos, "unfold might fail because the predicate " + pred.predicate.FullName + " does not hold."))), "unfold") :::
+ etran.InhaleFrom(List(definition), "unfold", false, etran.Heap.select(o, pred.predicate.FullName))
+ case unfld@Unfold(acc@RdAccess(pred@MemberAccess(e, f), nbEpsilons)) =>
+ val o = TrExpr(e);
+ var (definition, checkEpsilons) = nbEpsilons match {
+ case None => (EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), e), IntLiteral(1)), Nil)
+ case Some(None) => throw new Exception("Not supported yet!");
+ case Some(Some(i)) => (EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), e), i), isDefined(i) ::: bassert(Boogie.IntLiteral(0) <= i, s.pos, "Number of epsilons might be negative.") :: Nil)
+ }
+ Comment("unfold") ::
+ isDefined(e) :::
+ bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
+ checkEpsilons :::
+ Exhale(List((acc, ErrorMessage(s.pos, "Unold might fail because the predicate " + pred.predicate.FullName + " does not hold."))), "unfold") :::
+ etran.InhaleFrom(List(definition), "unfold", false, etran.Heap.select(o, pred.predicate.FullName))
+ case c@CallAsync(declaresLocal, token, obj, id, args) =>
+ val formalThisV = new Variable("this", new Type(c.m.Parent))
+ val formalThis = new VariableExpr(formalThisV)
+ val formalInsV = for (p <- c.m.ins) yield new Variable(p.id, p.t)
+ val formalIns = for (v <- formalInsV) yield new VariableExpr(v)
+
+ val (tokenV,tokenId) = NewBVar("token", tref, true)
+ val (asyncStateV,asyncState) = NewBVar("asyncstate", tint, true)
+ val (preCallMaskV, preCallMask) = NewBVar("preCallMask", tmask, true)
+ val (preCallHeapV, preCallHeap) = NewBVar("preCallHeap", theap, true)
+ val (argsSeqV, argsSeq) = NewBVar("argsSeq", tArgSeq, true)
+ val argsSeqLength = 1 + args.length;
+ Comment("call " + id) ::
+ // declare the local variable, if needed
+ { if (c.local == null)
+ List[Stmt]()
+ else
+ List(BLocal(Variable2BVarWhere(c.local))) } :::
+ // remember the value of the heap and mask
+ BLocal(preCallMaskV) :: (preCallMask := etran.Mask) ::
+ BLocal(preCallHeapV) :: (preCallHeap := etran.Heap) ::
+ BLocal(argsSeqV) ::
+ // introduce formal parameters and pre-state globals
+ (for (v <- formalThisV :: formalInsV) yield BLocal(Variable2BVarWhere(v))) :::
+ // check definedness of arguments
+ isDefined(obj) :::
+ bassert(nonNull(obj), c.pos, "The target of the method call might be null.") ::
+ (args flatMap { e: Expression => isDefined(e)}) :::
+ // assign actual ins to formal ins
+ (formalThis := obj) ::
+ (for ((v,e) <- formalIns zip args) yield (v := e)) :::
+ // insert all arguments in the argument sequence
+ Boogie.AssignMap(argsSeq, 0, formalThis) ::
+ { var i = 1
+ for (v <- formalIns) yield { val r = Boogie.AssignMap(argsSeq, i, v); i += 1; r }
+ } :::
+ // exhale preconditions
+ Exhale(Preconditions(c.m.spec) map
+ (p => SubstThisAndVars(p, formalThis, c.m.ins, formalIns)) zip (Preconditions(c.m.spec) map { p => ErrorMessage(c.pos, "The precondition at " + p.pos + " might not hold.")}), "precondition") :::
+ // create a new token
+ BLocal(tokenV) :: Havoc(tokenId) :: bassume(nonNull(tokenId)) ::
+ // the following assumes help in proving that the token is fresh
+ bassume(Heap.select(tokenId, "joinable") ==@ 0) ::
+ bassume(new Boogie.MapSelect(Mask, tokenId, "joinable", "perm$N")==@ 0) ::
+ bassume(new Boogie.MapSelect(Mask, tokenId, "joinable", "perm$R")==@ 0) ::
+ etran.IncPermission(tokenId, "joinable", 100) ::
+ // create a fresh value for the joinable field
+ BLocal(asyncStateV) :: Boogie.Havoc(asyncState) :: bassume(asyncState !=@ 0) ::
+ etran.Heap.store(tokenId, "joinable", asyncState) ::
+ // assume the pre call state for the token is the state before inhaling the precondition
+ bassume(CallHeap(asyncState) ==@ preCallHeap) ::
+ bassume(CallMask(asyncState) ==@ preCallMask) ::
+ bassume(CallArgs(asyncState) ==@ argsSeq) ::
+ // assign the returned token to the variable
+ { if (token != null) List(token := tokenId) else List() }
+ case jn@JoinAsync(lhs, token) =>
+ val formalThisV = new Variable("this", new Type(jn.m.Parent))
+ val formalThis = new VariableExpr(formalThisV)
+ val formalInsV = for (p <- jn.m.ins) yield new Variable(p.id, p.t)
+ val formalIns = for (v <- formalInsV) yield new VariableExpr(v)
+ val formalOutsV = for (p <- jn.m.outs) yield new Variable(p.id, p.t)
+ val formalOuts = for (v <- formalOutsV) yield new VariableExpr(v)
+
+ val (argsSeqV, argsSeq) = NewBVar("argsSeq", tArgSeq, true)
+ val (preCallHeapV, preCallHeap) = NewBVar("preCallHeap", theap, true);
+ val (preCallMaskV, preCallMask) = NewBVar("preCallMask", tmask, true);
+ val preGlobals = List(preCallHeap, preCallMask);
+ val postEtran = new ExpressionTranslator(List(etran.Heap, etran.Mask), preGlobals, currentClass);
+ Comment("join async") ::
+ // check that we did not join yet
+ bassert(CanWrite(token, "joinable"), jn.pos, "The joinable field might not be writable.") ::
+ bassert(etran.Heap.select(token, "joinable") !=@ 0, jn.pos, "The joinable field might not be true.") ::
+ // lookup token.joinable
+ BLocal(argsSeqV) :: (argsSeq := CallArgs(etran.Heap.select(token, "joinable"))) ::
+ // check that token is well-defined
+ isDefined(token) :::
+ // retrieve the call's pre-state from token.joinable
+ BLocal(preCallHeapV) :: (preCallHeap := CallHeap(etran.Heap.select(token, "joinable"))) ::
+ BLocal(preCallMaskV) :: (preCallMask := CallMask(etran.Heap.select(token, "joinable"))) ::
+ // introduce locals for the out parameters
+ (for (v <- formalThisV :: formalInsV ::: formalOutsV) yield BLocal(Variable2BVarWhere(v))) :::
+ // initialize the in parameters
+ (formalThis := new MapSelect(argsSeq, 0)) ::
+ { var i = 1
+ (formalIns map { v => val r = (v := new MapSelect(argsSeq, i)); i += 1; r })
+ } :::
+ // havoc formal outs
+ (for (v <- formalOuts) yield Havoc(v)) :::
+ // set joinable to false
+ etran.Heap.store(token, "joinable", 0) ::
+ etran.SetNoPermission(token, "joinable", etran.Mask) ::
+ // inhale postcondition of the call
+ postEtran.Inhale(Postconditions(jn.m.spec) map
+ { p => SubstThisAndVars(p, formalThis, jn.m.ins ++ jn.m.outs, formalIns ++ formalOuts)}, "postcondition", false) :::
+ // assign formal outs to actual outs
+ (for ((v,e) <- lhs zip formalOuts) yield (v :=e))
+ }
+ }
+
+ def translateAllocation(cl: Class, initialization: List[Init]): (Boogie.BVar, List[Boogie.Stmt]) = {
+ val (nw, nwe) = NewBVar("nw", Boogie.ClassType(cl), true)
+ val (ttV,tt) = Boogie.NewTVar("T")
+ val f = new Boogie.BVar("f", FieldType(tt))
+ (nw,
+ Comment("new") ::
+ BLocal(nw) :: Havoc(nwe) ::
+ bassume(nonNull(nwe) && (dtype(nwe) ==@ TrType(cl))) ::
+ bassume(new Boogie.Forall(ttV, f, etran.HasNoPermission(nwe, f.id))) ::
+ // initial values of fields:
+ bassume(etran.Heap.select(nwe, "mu") ==@ bLockBottom) ::
+ bassume(etran.Heap.select(nwe, "held") <= 0) ::
+ bassume(etran.Heap.select(nwe, "rdheld") ==@ false) ::
+ // give access to user-defined fields and special fields:
+ (for (f <- cl.Fields ++ RootClass.MentionableFields) yield
+ etran.IncPermission(nwe, f.FullName, 100)) :::
+ // initialize fields according to the initialization
+ (initialization flatMap { init => isDefined(init.e) ::: etran.Heap.store(nwe, init.f.FullName, init.e) })
+ )
+ }
+
+ def TrAcquire(s: Statement, nonNullObj: Expression) = {
+ val o = TrExpr(nonNullObj);
+ val (lastAcquireVar, lastAcquire) = Boogie.NewBVar("lastAcquire", Boogie.ClassType(IntClass), true)
+ val (lastSeenHeldV, lastSeenHeld) = Boogie.NewBVar("lastSeenHeld", tint, true)
+ val (lastSeenMuV, lastSeenMu) = Boogie.NewBVar("lastSeenMu", tmu, true)
+ bassert(CanRead(o, "mu"), s.pos, "The mu field of the target of the acquire statement might not be readable.") ::
+ bassert(etran.MaxLockIsBelowX(etran.Heap.select(o,"mu")), s.pos, "The mu field of the target of the acquire statement might not be above maxlock.") ::
+ bassume(etran.Heap.select(o,"mu") !=@ bLockBottom) :: // this isn't strictly necessary, it seems; but we might as well include it
+ // remember the state right before releasing
+ BLocal(lastSeenMuV) :: (lastSeenMu := etran.Heap.select(o, "mu")) ::
+ BLocal(lastSeenHeldV) :: Havoc(lastSeenHeld) :: (lastSeenHeld := etran.Heap.select(o, "held")) ::
+ bassume(! isHeld(o) && ! isRdHeld(o)) :: // this assume follows from the previous assert
+ // update the thread's locking state
+ BLocal(lastAcquireVar) :: Havoc(lastAcquire) :: bassume(0 < lastAcquire) ::
+ etran.SetFullPermission(o, "held") ::
+ etran.Heap.store(o, "held", lastAcquire) ::
+ InhaleInvariants(nonNullObj, false, etran.WhereOldIs(LastSeenHeap(lastSeenMu, lastSeenHeld), LastSeenMask(lastSeenMu, lastSeenHeld))) :::
+ // remember values of Heap/Mask globals (for proving history constraint at release)
+ bassume(AcquireHeap(lastAcquire) ==@ etran.Heap) ::
+ bassume(AcquireMask(lastAcquire) ==@ etran.Mask)
+ }
+ def TrRelease(s: Statement, nonNullObj: Expression) = {
+ val (heldV, held) = Boogie.NewBVar("held", tint, true)
+ val (prevLmV, prevLm) = Boogie.NewBVar("prevLM", tref, true)
+ val (preReleaseMaskV, preReleaseMask) = NewBVar("preReleaseMask", tmask, true)
+ val (preReleaseHeapV, preReleaseHeap) = NewBVar("preReleaseHeap", theap, true)
+ val o = TrExpr(nonNullObj);
+ BLocal(preReleaseMaskV) :: (preReleaseMask := etran.Mask) ::
+ BLocal(preReleaseHeapV) :: (preReleaseHeap := etran.Heap) ::
+ bassert(CanWrite(o, "held"), s.pos, "The held field of the target of the release statement might not be writable.") ::
+ bassert(isHeld(o), s.pos, "The target of the release statement might be not be locked by the current thread.") ::
+ bassert(!isRdHeld(o), s.pos, "Release might fail because the current thread might hold the read lock.") ::
+ ExhaleInvariants(nonNullObj, false, ErrorMessage(s.pos, "Monitor invariant might hot hold."), etran.WhereOldIs(AcquireHeap(etran.Heap.select(o, "held")), AcquireMask(etran.Heap.select(o, "held")))) :::
+ // havoc o.held where 0<=o.held
+ BLocal(heldV) :: Havoc(held) :: bassume(held <= 0) ::
+ etran.Heap.store(o, "held", held) ::
+ etran.SetNoPermission(o, "held", etran.Mask) ::
+ // assume a seen state is the one right before the share
+ bassume(LastSeenHeap(etran.Heap.select(o, "mu"), held) ==@ preReleaseHeap) ::
+ bassume(LastSeenMask(etran.Heap.select(o, "mu"), held) ==@ preReleaseMask)
+ }
+ def TrRdAcquire(s: Statement, nonNullObj: Expression) = {
+ val (heldV, held) = Boogie.NewBVar("held", tint, true)
+ val o = TrExpr(nonNullObj)
+ bassert(CanRead(o, "mu"), s.pos, "The mu field of the target of the read-acquire statement might not be readable.") ::
+ bassert(etran.MaxLockIsBelowX(etran.Heap.select(o, "mu")), s.pos, "The mu field of the target of the read-acquire statement might not be above maxlock.") ::
+ bassume(etran.Heap.select(o,"mu") !=@ bLockBottom) :: // this isn't strictly necessary, it seems; but we might as well include it
+ bassume(! isHeld(o) && ! isRdHeld(o)) ::
+ BLocal(heldV) :: Havoc(held) :: bassume(held <= 0) ::
+ etran.Heap.store(o, "held", held) ::
+ etran.Heap.store(o, "rdheld", true) ::
+ InhaleInvariants(nonNullObj, true)
+ }
+ def TrRdRelease(s: Statement, nonNullObj: Expression) = {
+ val (heldV, held) = Boogie.NewBVar("held", tint, true)
+ val o = TrExpr(nonNullObj);
+ bassert(isRdHeld(o), s.pos, "The current thread might not hold the read-lock of the object being released.") ::
+ ExhaleInvariants(nonNullObj, true, ErrorMessage(s.pos, "Monitor invariant might not hold.")) :::
+ BLocal(heldV) :: Havoc(held) :: bassume(held <= 0) ::
+ etran.Heap.store(o, "held", held) ::
+ etran.Heap.store(o, "rdheld", false)
+ }
+
+ def translateCall(c: Call): List[Stmt] = {
+ val obj = c.obj;
+ val lhs = c.lhs;
+ val id = c.id;
+ val args = c.args;
+ val formalThisV = new Variable("this", new Type(c.m.Parent))
+ val formalThis = new VariableExpr(formalThisV)
+ val formalInsV = for (p <- c.m.ins) yield new Variable(p.id, p.t)
+ val formalIns = for (v <- formalInsV) yield new VariableExpr(v)
+ val formalOutsV = for (p <- c.m.outs) yield new Variable(p.id, p.t)
+ val formalOuts = for (v <- formalOutsV) yield new VariableExpr(v)
+ val preGlobals = etran.FreshGlobals("call")
+ val postEtran = etran.FromPreGlobals(preGlobals)
+ Comment("call " + id) ::
+ // introduce formal parameters and pre-state globals
+ (for (v <- formalThisV :: formalInsV ::: formalOutsV) yield BLocal(Variable2BVarWhere(v))) :::
+ (for (v <- preGlobals) yield BLocal(v)) :::
+ // remember values of globals
+ (for ((o,g) <- preGlobals zip etran.Globals) yield (new Boogie.VarExpr(o) := g)) :::
+ // check definedness of arguments
+ isDefined(obj) :::
+ bassert(nonNull(obj), c.pos, "The target of the method call might be null.") ::
+ (args flatMap { e: Expression => isDefined(e)}) :::
+ // assign actual ins to formal ins
+ (formalThis := obj) ::
+ (for ((v,e) <- formalIns zip args) yield (v := e)) :::
+ // exhale preconditions
+ Exhale(Preconditions(c.m.spec) map
+ (p => SubstThisAndVars(p, formalThis, c.m.ins, formalIns)) zip (Preconditions(c.m.spec) map { p => ErrorMessage(c.pos, "The precondition at " + p.pos + " might not hold.")}), "precondition") :::
+ // havoc formal outs
+ (for (v <- formalOuts) yield Havoc(v)) :::
+ // havoc lockchanges
+ LockHavoc(for (e <- LockChanges(c.m.spec) map (p => SubstThisAndVars(p, formalThis, c.m.ins, formalIns))) yield etran.Tr(e), postEtran) :::
+ // inhale postconditions (using the state before the call as the "old" state)
+ postEtran.Inhale(Postconditions(c.m.spec) map
+ (p => SubstThisAndVars(p, formalThis, c.m.ins ++ c.m.outs, formalIns ++ formalOuts)) , "postcondition", false) :::
+ // assign formal outs to actual outs
+ (for ((v,e) <- lhs zip formalOuts) yield (v :=e))
+ }
+
+ def translateWhile(w: WhileStmt): List[Stmt] = {
+ val guard = w.guard;
+ val invs = w.invs;
+ val lkch = w. lkch;
+ val body = w.body;
+
+ val preLoopGlobals = etran.FreshGlobals("while")
+ val loopEtran = etran.FromPreGlobals(preLoopGlobals)
+ val iterStartGlobals = etran.FreshGlobals("iterStart")
+ val iterStartEtran = etran.FromPreGlobals(iterStartGlobals)
+ val saveLocalsV = for (v <- w.LoopTargetsList) yield new Variable(v.id, v.t)
+ val iterStartLocalsV = for (v <- w.LoopTargetsList) yield new Variable(v.id, v.t)
+ val lkchOld = lkch map (e => SubstVars(e, w.LoopTargetsList,
+ for (v <- saveLocalsV) yield new VariableExpr(v)))
+ val lkchIterStart = lkch map (e => SubstVars(e, w.LoopTargetsList,
+ for (v <- iterStartLocalsV) yield new VariableExpr(v)))
+ val oldLocks = lkchOld map (e => loopEtran.oldEtran.Tr(e))
+ val iterStartLocks = lkchIterStart map (e => iterStartEtran.oldEtran.Tr(e))
+ val newLocks = lkch map (e => loopEtran.Tr(e));
+ Comment("while") ::
+ // save globals
+ (for (v <- preLoopGlobals) yield BLocal(v)) :::
+ (loopEtran.oldEtran.Heap := loopEtran.Heap) ::
+ (loopEtran.oldEtran.Mask := loopEtran.Mask) :: // oldMask is not actually used below
+ // check invariant on entry to the loop
+ Exhale(invs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant might not hold on entry to the loop."))}, "loop invariant, initially") :::
+ // save values of local-variable loop targets
+ (for (sv <- saveLocalsV) yield BLocal(Variable2BVarWhere(sv))) :::
+ (for ((v,sv) <- w.LoopTargetsList zip saveLocalsV) yield
+ (new VariableExpr(sv) := new VariableExpr(v))) :::
+ // havoc local-variable loop targets
+ (w.LoopTargets :\ List[Boogie.Stmt]()) ( (v,vars) => (v match {
+ case v: ImmutableVariable => Boogie.Havoc(Boogie.VarExpr("assigned$" + v.id))
+ case _ => Boogie.Havoc(Boogie.VarExpr(v.UniqueName)) }) :: vars) :::
+ Boogie.If(null,
+ // 1. CHECK DEFINEDNESS OF INVARIANT
+ Comment("check loop invariant definedness") ::
+ //(w.LoopTargets.toList map { v: Variable => Boogie.Havoc(Boogie.VarExpr(v.id)) }) :::
+ Boogie.Havoc(etran.Heap) :: Boogie.Assign(etran.Mask, ZeroMask) ::
+ InhaleWithChecking(invs, "loop invariant definedness") :::
+ bassume(false)
+ , Boogie.If(null,
+ // 2. CHECK LOOP BODY
+ // Renew Heap and Mask: set Mask to ZeroMask, and havoc Heap everywhere except
+ // at {old(local),local}.{held,rdheld}
+ Havoc(etran.Heap) :: (etran.Mask := ZeroMask) ::
+ Inhale(invs, "loop invariant, body") :::
+ // this is the state at the beginning of the loop iteration; save these values
+ (for (v <- iterStartGlobals) yield BLocal(v)) :::
+ (iterStartEtran.oldEtran.Heap := iterStartEtran.Heap) ::
+ (iterStartEtran.oldEtran.Mask := iterStartEtran.Mask) :: // oldMask is not actually used below
+ (for (isv <- iterStartLocalsV) yield BLocal(Variable2BVarWhere(isv))) :::
+ (for ((v,isv) <- w.LoopTargetsList zip iterStartLocalsV) yield
+ (new VariableExpr(isv) := new VariableExpr(v))) :::
+ // evaluate the guard
+ isDefined(guard) ::: List(bassume(guard)) :::
+ translateStatement(body) :::
+ // check invariant
+ Exhale(invs map { inv => (inv, ErrorMessage(w.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained") :::
+ isLeaking(w.pos, "The loop might leak refereces.") :::
+ // enforce lockchange
+ (NumberOfLocksHeldIsInvariant(iterStartLocks, newLocks, iterStartEtran) map { e: Boogie.Expr => bassert(e, w.pos, "The loop might lock/unlock more than the changelock clause allows.") }) :::
+ bassume(false),
+ // 3. AFTER LOOP
+ LockHavoc(oldLocks ++ newLocks, loopEtran) :::
+ (NumberOfLocksHeldIsInvariant(oldLocks, newLocks, loopEtran) map bassume) :::
+ Inhale(invs, "loop invariant, after loop") :::
+ bassume(!guard)))
+ }
+
+ def UpdateMu(o: Expr, allowOnlyFromBottom: boolean,
+ lowerBounds: List[Expression], upperBounds: List[Expression], error: ErrorMessage): List[Stmt] = {
+ def BoundIsNullObject(b: Expression): Boogie.Expr = {
+ if (b.typ.IsMu) false else b ==@ bnull
+ }
+ def MuValue(b: Expression): Expr = {
+ if (b.typ.IsMu) b else etran.Heap.select(b, "mu")
+ }
+ def Below(a: Expr, b: Expr) = {
+ new FunctionApp("MuBelow", a, b)
+ }
+ val (muV, mu) = Boogie.NewBVar("mu", Boogie.NamedType("Mu"), true)
+ // check that bounds are well-defined
+ ((lowerBounds ++ upperBounds) flatMap { bound => isDefined(bound)}) :::
+ // check that we have full access to mu
+ bassert(CanWrite(o, "mu"), error.pos, error.message + " The mu field of the target might not be writable.") ::
+ // ...and that mu starts off as lockbottom, if desired
+ (if (allowOnlyFromBottom)
+ List(bassert(etran.Heap.select(o,"mu") ==@ bLockBottom,
+ error.pos, error.message + " The object may already be shared (i.e., mu may not be LockBottom)"))
+ else
+ List()) :::
+ // check for each bound that if it is a non-null object, then its mu field is readable
+ (for (bound <- lowerBounds ++ upperBounds if !bound.typ.IsMu) yield
+ bassert((bound ==@ bnull) || CanRead(bound, "mu"), bound.pos, "The mu field of bound at " + bound.pos + " might not be readable." )) :::
+ // check that each lower bound is smaller than each upper bound
+ (for (lb <- lowerBounds; ub <- upperBounds) yield
+ bassert( (etran.ShaveOffOld(lb), etran.ShaveOffOld(ub)) match {
+ case ((MaxLockLiteral(),o0), (MaxLockLiteral(),o1)) =>
+ if (o0 == o1)
+ false
+ else
+ etran.TemporalMaxLockComparison(etran.ChooseEtran(o0), etran.ChooseEtran(o1))
+ case ((MaxLockLiteral(),o), _) => etran.ChooseEtran(o).MaxLockIsBelowX(MuValue(ub))
+ case (_, (MaxLockLiteral(),o)) => etran.ChooseEtran(o).MaxLockIsAboveX(MuValue(lb))
+ case _ => BoundIsNullObject(lb) ||
+ BoundIsNullObject(ub) ||
+ Below(MuValue(lb), MuValue(ub)) }, lb.pos, "The lower bound at " + lb.pos + " might not be smaller than the upper bound at " + ub.pos + ".")) :::
+ // havoc o.mu
+ BLocal(muV) :: Havoc(mu) :: bassume(mu !=@ bLockBottom) ::
+ // assume that o.mu is between the given bounds (or above maxlock if no bounds are given)
+ (if (lowerBounds == Nil && upperBounds == Nil) {
+ // assume maxlock << o.mu
+ List(bassume(etran.MaxLockIsBelowX(mu)))
+ } else {
+ (for (lb <- lowerBounds) yield
+ // assume lb << o.mu
+ bassume(
+ if (etran.IsMaxLockLit(lb)) {
+ val (f,o) = etran.ShaveOffOld(lb)
+ etran.ChooseEtran(o).MaxLockIsBelowX(mu)
+ } else
+ (BoundIsNullObject(lb) || Below(MuValue(lb), mu)))) :::
+ (for (ub <- upperBounds) yield
+ // assume o.mu << ub
+ bassume(
+ if (etran.IsMaxLockLit(ub)) {
+ val (f,o) = etran.ShaveOffOld(ub)
+ etran.ChooseEtran(o).MaxLockIsAboveX(mu)
+ } else
+ (BoundIsNullObject(ub) || Below(mu, MuValue(ub)))))
+ }) :::
+ // store the mu field
+ etran.Heap.store(o, "mu", mu)
+ }
+
+ def isLeaking(pos: Position, msg: String): List[Boogie.Stmt] = {
+ if(checkLeaks) {
+ var o = Boogie.VarExpr("$o");
+ var f = "$f";
+ val (ttV,tt) = Boogie.NewTVar("T")
+ List(
+ bassert(new Boogie.Forall(
+ List(ttV),
+ List(Boogie.BVar("$o", tref), Boogie.BVar("$f", FieldType(tt))),
+ Nil,
+ (o ==@ bnull) || ((new MapSelect(etran.Mask, o, f, "perm$R") ==@ 0) && (new MapSelect(etran.Mask, o, f, "perm$N") ==@ 0))
+ ), pos, msg)
+ )
+ } else {
+ Nil
+ }
+ }
+
+ def LockFrame(lkch: List[Expression], etran: ExpressionTranslator) =
+ LocksUnchanged(for (l <- lkch) yield etran.Tr(l), etran)
+ def LocksUnchanged(exceptions: List[Boogie.Expr], etran: ExpressionTranslator) = {
+ val (lkV, lk) = Boogie.NewBVar("lk", tref, true)
+ val b: Boogie.Expr = false
+ new Boogie.Forall(List(lkV),
+ List(etran.Heap.select(lk, "held"), etran.Heap.select(lk, "rdheld")),
+ (((0 < Boogie.MapSelect(etran.Heap, lk, "held")) ==@
+ (0 < Boogie.MapSelect(etran.oldEtran.Heap, lk, "held"))) &&
+ (Boogie.MapSelect(etran.Heap, lk, "rdheld") ==@
+ Boogie.MapSelect(etran.oldEtran.Heap, lk, "rdheld"))) ||
+ ((exceptions :\ b) ((e,ll) => ll || (lk ==@ e))))
+ }
+ def LockHavoc(locks: List[Boogie.Expr], etran: ExpressionTranslator) = {
+ val (heldV, held) = NewBVar("isHeld", Boogie.ClassType(IntClass), true)
+ val (rdheldV, rdheld) = NewBVar("isRdHeld", Boogie.ClassType(BoolClass), true)
+ BLocal(heldV) :: BLocal(rdheldV) ::
+ List.flatten (for (o <- locks) yield { // todo: somewhere we should worry about Df(l)
+ Havoc(held) :: Havoc(rdheld) ::
+ bassume(rdheld ==> (0 < held)) ::
+ MapUpdate(etran.Heap, o, "held", held) ::
+ MapUpdate(etran.Heap, o, "rdheld", rdheld) })
+ }
+ def NumberOfLocksHeldIsInvariant(oldLocks: List[Boogie.Expr], newLocks: List[Boogie.Expr],
+ etran: ExpressionTranslator) = {
+ List.flatten (for ((o,n) <- oldLocks zip newLocks) yield {
+ // oo.held == nn.held && oo.rdheld == nn.rdheld
+ (((0 < Boogie.MapSelect(etran.oldEtran.Heap, o, "held")) ==@
+ (0 < Boogie.MapSelect(etran.Heap, n, "held"))) &&
+ (Boogie.MapSelect(etran.oldEtran.Heap, o, "rdheld") ==@
+ Boogie.MapSelect(etran.Heap, n, "rdheld"))) ::
+ // no.held == on.held && no.rdheld == on.rdheld
+ (((0 < Boogie.MapSelect(etran.Heap, o, "held")) ==@
+ (0 < Boogie.MapSelect(etran.oldEtran.Heap, n, "held"))) &&
+ (Boogie.MapSelect(etran.Heap, o, "rdheld") ==@
+ Boogie.MapSelect(etran.oldEtran.Heap, n, "rdheld"))) ::
+ // o == n || (oo.held != no.held && (!oo.rdheld || !no.rdheld))
+ ((o ==@ n) ||
+ (((0 < Boogie.MapSelect(etran.oldEtran.Heap, o, "held")) !=@ (0 < Boogie.MapSelect(etran.Heap, o, "held"))) &&
+ ((! Boogie.MapSelect(etran.oldEtran.Heap, o, "rdheld")) ||
+ (! Boogie.MapSelect(etran.Heap, o, "rdheld"))))) ::
+ Nil
+ })
+ }
+
+ implicit def lift(s: Stmt): List[Stmt] = List(s)
+ def isDefined(e: Expression) = etran.isDefined(e)(true)
+ def TrExpr(e: Expression) = etran.Tr(e)
+
+ def InhaleInvariants(obj: Expression, readonly: boolean, tran: ExpressionTranslator) = {
+ val shV = new Variable("sh", new Type(obj.typ))
+ val sh = new VariableExpr(shV)
+ BLocal(Variable2BVar(shV)) :: Boogie.Assign(TrExpr(sh), TrExpr(obj)) ::
+ tran.Inhale(obj.typ.Invariants map
+ (inv => SubstThis(inv.e, sh)) map
+ (inv => (if (readonly) SubstRd(inv) else inv)), "monitor invariant", false)
+ }
+ def ExhaleInvariants(obj: Expression, readonly: boolean, msg: ErrorMessage, tran: ExpressionTranslator) = {
+ val shV = new Variable("sh", new Type(obj.typ))
+ val sh = new VariableExpr(shV)
+ BLocal(Variable2BVar(shV)) :: Boogie.Assign(TrExpr(sh), TrExpr(obj)) ::
+ tran.Exhale(obj.typ.Invariants map
+ (inv => SubstThis(inv.e, sh)) map
+ (inv => (if (readonly) SubstRd(inv) else inv, msg)), "monitor invariant", false)
+ }
+ def InhaleInvariants(obj: Expression, readonly: boolean) = {
+ val shV = new Variable("sh", new Type(obj.typ))
+ val sh = new VariableExpr(shV)
+ BLocal(Variable2BVar(shV)) :: Boogie.Assign(TrExpr(sh), TrExpr(obj)) ::
+ Inhale(obj.typ.Invariants map
+ (inv => SubstThis(inv.e, sh)) map
+ (inv => (if (readonly) SubstRd(inv) else inv)), "monitor invariant")
+ }
+ def ExhaleInvariants(obj: Expression, readonly: boolean, msg: ErrorMessage) = {
+ val shV = new Variable("sh", new Type(obj.typ))
+ val sh = new VariableExpr(shV)
+ BLocal(Variable2BVar(shV)) :: Boogie.Assign(TrExpr(sh), TrExpr(obj)) ::
+ Exhale(obj.typ.Invariants map
+ (inv => SubstThis(inv.e, sh)) map
+ (inv => (if (readonly) SubstRd(inv) else inv, msg)), "monitor invariant")
+ }
+
+ def Inhale(predicates: List[Expression], occasion: String): List[Boogie.Stmt] = etran.Inhale(predicates, occasion, false)
+ def Exhale(predicates: List[(Expression, ErrorMessage)], occasion: String): List[Boogie.Stmt] = etran.Exhale(predicates, occasion, false)
+ def InhaleWithChecking(predicates: List[Expression], occasion: String): List[Boogie.Stmt] = etran.Inhale(predicates, occasion, true)
+ def ExhaleWithChecking(predicates: List[(Expression, ErrorMessage)], occasion: String): List[Boogie.Stmt] = etran.Exhale(predicates, occasion, true)
+
+ def CanRead(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = etran.CanRead(obj, field)
+ def CanWrite(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = etran.CanWrite(obj, field)
+
+
+ /**********************************************************************
+ ***************** EXPRESSIONS *****************
+ **********************************************************************/
+
+class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.Expr], currentClass: Class) {
+ import TranslationHelper._
+ import TranslationOptions._
+
+ val Heap = globals(0);
+ val Mask = globals(1);
+ lazy val oldEtran = new ExpressionTranslator(preGlobals, preGlobals, currentClass)
+ var checkTermination = false; // check that heap required by callee is strictly smaller than heap required by caller
+
+ def this(globals: List[Boogie.Expr], cl: Class) = this(globals, globals map (g => Boogie.Old(g)), cl)
+ def this(cl: Class) = this(for ((id,t) <- S_ExpressionTranslator.Globals) yield Boogie.VarExpr(id), cl)
+
+ def Globals = List(Heap, Mask)
+ def ChooseEtran(chooseOld: boolean) = if (chooseOld) oldEtran else this
+ // Create a list of fresh global variables
+ def FreshGlobals(prefix: String) = {
+ new Boogie.BVar(prefix + "Heap", theap, true) ::
+ new Boogie.BVar(prefix + "Mask", tmask, true) ::
+ Nil
+ }
+
+ // Create a new ExpressionTranslator that is a copy of the receiver, but with
+ // preGlobals as the old global variables
+ def FromPreGlobals(preGlobals: List[Boogie.BVar]) = {
+ val g = for ((id,t) <- S_ExpressionTranslator.Globals) yield VarExpr(id)
+ val pg = preGlobals map (g => new VarExpr(g))
+ new ExpressionTranslator(g, pg, currentClass)
+ }
+
+ def UseCurrentAsOld() = {
+ new ExpressionTranslator(globals, globals, currentClass);
+ }
+
+ def WhereOldIs(h: Boogie.Expr, m: Boogie.Expr) = {
+ new ExpressionTranslator(globals, List(h, m), currentClass);
+ }
+
+ /**********************************************************************
+ ***************** TR/DF *****************
+ **********************************************************************/
+
+ def isDefined(e: Expression)(implicit assumption: Expr): List[Boogie.Stmt] = {
+ def prove(goal: Expr, pos: Position, msg: String)(implicit assumption: Expr): Boogie.Assert = {
+ bassert(assumption ==> goal, pos, msg)
+ }
+ e match {
+ case IntLiteral(n) => Nil
+ case BoolLiteral(b) => Nil
+ case NullLiteral() => Nil
+ case MaxLockLiteral() => Nil
+ case LockBottomLiteral() => Nil
+ case _:ThisExpr => Nil
+ case _:Result => Nil
+ case _:VariableExpr => Nil
+ case fs @ MemberAccess(e, f) =>
+ assert(!fs.isPredicate);
+ 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 Holds(e) =>
+ isDefined(e)
+ case RdHolds(e) =>
+ isDefined(e)
+ case _: Assigned => Nil
+ case Old(e) =>
+ oldEtran.isDefined(e)
+ case IfThenElse(con, then, els) =>
+ isDefined(con) ::: Boogie.If(Tr(con), isDefined(then), isDefined(els))
+ case Not(e) =>
+ isDefined(e)
+ case func@FunctionApplication(obj, id, args) =>
+ val newGlobals = FreshGlobals("checkPre");
+ val (tmpHeapV, tmpHeap) = Boogie.NewBVar("Heap", theap, true);
+ val (tmpMaskV, tmpMask) = Boogie.NewBVar("Mask", tmask, true);
+ val tmpTranslator = new ExpressionTranslator(List(tmpHeap,tmpMask), currentClass);
+ // check definedness of receiver + arguments
+ (obj :: args flatMap { arg => isDefined(arg) }) :::
+ // check that receiver is not null
+ List(prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.")) :::
+ // check precondition of the function by exhaling the precondition in tmpHeap/tmpMask
+ Comment("check precondition of call") ::
+ bassume(assumption) ::
+ BLocal(tmpHeapV) :: (tmpHeap := Heap) ::
+ BLocal(tmpMaskV) :: (tmpMask := Mask) :::
+ tmpTranslator.Exhale(Preconditions(func.f.spec) map { pre=> (SubstThisAndVars(pre, obj, func.f.ins, args), ErrorMessage(func.pos, "Precondition at " + pre.pos + " might not hold."))},
+ "function call",
+ false) :::
+ // size of the heap of callee must be strictly smaller than size of the heap of the caller
+ (if(checkTermination) { List(prove(NonEmptyMask(tmpMask), func.pos, "The heap of the callee might not be strictly smaller than the heap of the caller.")) } else Nil)
+ case unfolding@Unfolding(access, e) =>
+ val (checks, predicate, definition, from) = access match {
+ case acc@Access(pred@MemberAccess(obj, f), perm) =>
+ val receiverOk = isDefined(obj) ::: prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.");
+ val body = SubstThis(DefinitionOf(pred.predicate), obj);
+ perm match {
+ case None => (receiverOk, acc, body, Heap.select(Tr(obj), pred.predicate.FullName))
+ case Some(fraction) => (receiverOk ::: isDefined(fraction) ::: prove(0 <= Tr(fraction), fraction.pos, "Fraction might be negative") :: prove(Tr(fraction) <= 100, fraction.pos, "Fraction might exceed 100."), acc, FractionOf(body, fraction), Heap.select(Tr(obj), pred.predicate.FullName))
+ }
+ case acc@RdAccess(pred@MemberAccess(obj, f), perm) =>
+ val receiverOk = isDefined(obj) ::: prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.");
+ val body = SubstThis(DefinitionOf(pred.predicate), obj);
+ perm match {
+ case None => (receiverOk, acc, EpsilonsOf(body, IntLiteral(1)), Heap.select(Tr(obj), pred.predicate.FullName))
+ case Some(None) => assert(false); (null, null, null, Heap.select(Tr(obj), pred.predicate.FullName))
+ case Some(Some(epsilons)) => (receiverOk ::: isDefined(epsilons) ::: prove(0 <= Tr(epsilons), epsilons.pos, "Number of epsilons might be negative"), acc, EpsilonsOf(body, epsilons), Heap.select(Tr(obj), pred.predicate.FullName))
+ }
+ }
+ val newGlobals = FreshGlobals("checkPre");
+ val (tmpHeapV, tmpHeap) = Boogie.NewBVar("Heap", theap, true);
+ val (tmpMaskV, tmpMask) = Boogie.NewBVar("Mask", tmask, true);
+ val tmpTranslator = new ExpressionTranslator(List(tmpHeap, tmpMask), currentClass);
+ Comment("unfolding") ::
+ // check definedness
+ checks :::
+ // copy state into temporary variables
+ BLocal(tmpHeapV) :: Boogie.Assign(tmpHeap, Heap) ::
+ BLocal(tmpMaskV) :: Boogie.Assign(tmpMask, Mask) ::
+ // exhale the predicate
+ tmpTranslator.Exhale(List((predicate, ErrorMessage(unfolding.pos, "Unfolding might fail."))), "unfolding", false) :::
+ // inhale the definition of the predicate
+ tmpTranslator.InhaleFrom(List(definition), "unfolding", false, from) :::
+ // check definedness of e in state where the predicate is unfolded
+ tmpTranslator.isDefined(e)
+ case Iff(e0,e1) =>
+ isDefined(e0) ::: isDefined(e1)
+ case Implies(e0,e1) =>
+ isDefined(e0) ::: isDefined(e1)(assumption && Tr(e0))
+ case And(e0,e1) =>
+ isDefined(e0) ::: isDefined(e1)(assumption && Tr(e0))
+ case Or(e0,e1) =>
+ isDefined(e0) ::: isDefined(e1)(assumption && Boogie.UnaryExpr("!", Tr(e0)))
+ case LockBelow(e0,e1) =>
+ var df = isDefined(e0) ::: isDefined(e1);
+ if (e0.typ.IsRef) {
+ df = df ::: List(prove(nonNull(Tr(e0)), e0.pos, "Receiver might be null."), prove(CanRead(Tr(e0),"mu"), e0.pos, "The mu field might not be readable."));
+ }
+ if (e1.typ.IsRef) {
+ df = df ::: List(prove(nonNull(Tr(e1)), e1.pos, "Receiver might be null."), prove(CanRead(Tr(e1),"mu"), e1.pos, "The mu field might not be readable."));
+ }
+ df
+ case e: CompareExpr =>
+ isDefined(e.E0) ::: isDefined(e.E1)
+ case Div(e0,e1) =>
+ isDefined(e0) ::: isDefined(e1) :::
+ List(prove(Tr(e1) !=@ 0, e1.pos, "Denominator might be zero."))
+ case Mod(e0,e1) =>
+ isDefined(e0) ::: isDefined(e1) ::: List(prove(Tr(e1) !=@ 0, e1.pos, "Denominator might be zero."))
+ case e: ArithmeticExpr =>
+ isDefined(e.E0) ::: isDefined(e.E1)
+ case q@Forall(i, Range(min, max), e) =>
+ // optimize for range
+ isDefinedForall(q.variables, min, max, e)
+ case q@Forall(i, seq, e) =>
+ var newVars = Nil : List[Variable];
+ for(i <- q.variables) {
+ newVars = newVars + new Variable(i.UniqueName, new Type(IntClass))
+ }
+ isDefinedForall(newVars, IntLiteral(0), Length(seq), SubstVars(e, q.variables, newVars map {newVar => At(seq, new VariableExpr(newVar)) }))
+ case EmptySeq(t) => Nil
+ case ExplicitSeq(es) =>
+ es flatMap { e => isDefined(e) }
+ case Range(min, max) =>
+ isDefined(min) ::: isDefined(max)
+ case Append(e0, e1) =>
+ isDefined(e0) ::: isDefined(e1)
+ case at@At(e0, e1) =>
+ isDefined(e0) ::: isDefined(e1) ::: List(prove(0 <= Tr(e1), at.pos, "Sequence index might be negative."), prove(Tr(e1) < Boogie.FunctionApp("Seq#Length", List(Tr(e0))), at.pos, "Sequence index might be larger than or equal to the length of the sequence."))
+ case Drop(e0, e1) =>
+ isDefined(e0) ::: isDefined(e1) ::: List(prove(0 <= Tr(e1), e.pos, "Cannot drop less than zero elements."), prove(Tr(e1) <= Boogie.FunctionApp("Seq#Length", List(Tr(e0))), e.pos, "Cannot drop more than elements than the length of the sequence."))
+ case Take(e0, e1) =>
+ isDefined(e0) ::: isDefined(e1) ::: List(prove(0 <= Tr(e1), e.pos, "Cannot take less than zero elements."), prove(Tr(e1) <= Boogie.FunctionApp("Seq#Length", List(Tr(e0))), e.pos, "Cannot take more than elements than the length of the sequence."))
+ case Length(e) =>
+ isDefined(e)
+ case Eval(h, e) =>
+ val (evalHeap, evalMask, checks, assumptions) = fromEvalState(h);
+ val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask), currentClass);
+ evalEtran.isDefined(e)
+ }
+ }
+
+ def isDefinedForall(is: List[Variable], min: Expression, max: Expression, e: Expression)(implicit assumption: Expr): List[Stmt] = {
+ var iTmps = Nil: List[Variable];
+ var assumption2 = assumption;
+ for(i <- is) {
+ val iTmp = new Variable(i.UniqueName, new Type(IntClass));
+ iTmps = iTmps + iTmp;
+ assumption2 = assumption2 && (Tr(min)<=VarExpr(iTmp.UniqueName)) && (VarExpr(iTmp.UniqueName) < Tr(max))
+ }
+ // check definedness of the bounds
+ isDefined(min) ::: isDefined(max) :::
+ // introduce a new local iTmp with an arbitrary value
+ (iTmps map { iTmp =>
+ BLocal(Boogie.BVar(iTmp.UniqueName, Boogie.NamedType("int")))
+ }) :::
+ // prove that the body is well-defined for iTmp, provided iTmp lies betweeen min and max
+ isDefined(SubstVars(e, is, iTmps map { iTmp => new VariableExpr(iTmp)}))(assumption2)
+ }
+
+ def Tr(e: Expression): Boogie.Expr = e match {
+ case IntLiteral(n) => n
+ case BoolLiteral(b) => b
+ case NullLiteral() => bnull
+ case MaxLockLiteral() => throw new Exception("maxlock case should be handled in << and == and !=")
+ case LockBottomLiteral() => bLockBottom
+ case _:ThisExpr => VarExpr("this")
+ case _:Result => VarExpr("result")
+ case ve : VariableExpr => VarExpr(ve.v.UniqueName)
+ case fs @ MemberAccess(e,_) =>
+ assert(! fs.isPredicate);
+ var r = Heap.select(Tr(e), fs.f.FullName);
+ if (fs.f.isInstanceOf[SpecialField] && fs.f.id == "joinable")
+ 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 Holds(e) =>
+ (0 < Heap.select(Tr(e), "held")) &&
+ !Heap.select(Tr(e), "rdheld")
+ case RdHolds(e) =>
+ Heap.select(Tr(e), "rdheld")
+ case a: Assigned =>
+ VarExpr("assigned$" + a.v.UniqueName)
+ case Old(e) =>
+ oldEtran.Tr(e)
+ case IfThenElse(con, then, els) =>
+ Boogie.Ite(Tr(con), Tr(then), Tr(els)) // of type: VarExpr(TrClass(then.typ))
+ case Not(e) =>
+ ! Tr(e)
+ case func@FunctionApplication(obj, id, args) =>
+ FunctionApp("#" + func.f.Parent.id + "." + id, Heap :: Mask :: (obj :: args map { arg => Tr(arg)}))
+ case uf@Unfolding(_, e) =>
+ Tr(e)
+ case Iff(e0,e1) =>
+ Tr(e0) <==> Tr(e1)
+ case Implies(e0,e1) =>
+ Tr(e0) ==> Tr(e1)
+ case And(e0,e1) =>
+ Tr(e0) && Tr(e1)
+ case Or(e0,e1) =>
+ Tr(e0) || Tr(e1)
+ case Eq(e0,e1) =>
+ (ShaveOffOld(e0), ShaveOffOld(e1)) match {
+ case ((MaxLockLiteral(),o0), (MaxLockLiteral(),o1)) =>
+ if (o0 == o1)
+ true
+ else
+ MaxLockPreserved
+ case ((MaxLockLiteral(),o), (fs@MemberAccess(q, "mu"), useOld)) => isHeldInHeap(Tr(q), ChooseEtran(useOld).Heap) && ChooseEtran(o).MaxLockEqualsX(Tr(fs))
+ case ((MaxLockLiteral(),o), _) => ChooseEtran(o).MaxLockEqualsX(Tr(e1))
+ case (_, (MaxLockLiteral(),o)) => ChooseEtran(o).MaxLockEqualsX(Tr(e0))
+ case _ => if(e0.typ.IsSeq) FunctionApp("Seq#Equal", List(Tr(e0), Tr(e1))) else (Tr(e0) ==@ Tr(e1))
+ }
+ case Neq(e0,e1) =>
+ if (IsMaxLockLit(e0) || IsMaxLockLit(e1))
+ Tr(Not(Eq(e0,e1)))
+ else
+ (Tr(e0) !=@ Tr(e1))
+ case Less(e0,e1) =>
+ Tr(e0) < Tr(e1)
+ case AtMost(e0,e1) =>
+ Tr(e0) <= Tr(e1)
+ case AtLeast(e0,e1) =>
+ Tr(e0) >= Tr(e1)
+ case Greater(e0,e1) =>
+ Tr(e0) > Tr(e1)
+ case LockBelow(e0,e1) => {
+ def MuValue(b: Expression): Boogie.Expr =
+ if (b.typ.IsRef) Boogie.MapSelect(Heap, Tr(b), "mu") else Tr(b)
+ (ShaveOffOld(e0), ShaveOffOld(e1)) match {
+ case ((MaxLockLiteral(),o0), (MaxLockLiteral(),o1)) =>
+ if (o0 == o1)
+ false
+ else
+ TemporalMaxLockComparison(ChooseEtran(o0), ChooseEtran(o1))
+ case ((MaxLockLiteral(),o), _) => ChooseEtran(o).MaxLockIsBelowX(MuValue(e1))
+ case (_, (MaxLockLiteral(),o)) => ChooseEtran(o).MaxLockIsAboveX(MuValue(e0))
+ case _ => new FunctionApp("MuBelow", MuValue(e0), MuValue(e1)) }
+ }
+ case Plus(e0,e1) =>
+ Tr(e0) + Tr(e1)
+ case Minus(e0,e1) =>
+ Tr(e0) - Tr(e1)
+ case Times(e0,e1) =>
+ Tr(e0) * Tr(e1)
+ case Div(e0,e1) =>
+ Tr(e0) / Tr(e1)
+ case Mod(e0,e1) =>
+ Tr(e0) % Tr(e1)
+ case q@Forall(is, Range(min, max), e) =>
+ // optimize translation for range expressions
+ translateForall(q.variables, min, max, e)
+ case q@Forall(is, seq, e) =>
+ var newVars = Nil : List[Variable];
+ for(i <- q.variables) {
+ newVars = newVars + new Variable(i.UniqueName, new Type(IntClass))
+ }
+ translateForall(newVars, IntLiteral(0), Length(seq), SubstVars(e, q.variables, newVars map {newVar => At(seq, new VariableExpr(newVar)) }))
+ case EmptySeq(t) =>
+ createEmptySeq
+ case ExplicitSeq(es) =>
+ es match {
+ case Nil => createEmptySeq
+ case h :: Nil => createSingletonSeq(Tr(h))
+ case h :: t => createAppendSeq(createSingletonSeq(Tr(h)), Tr(ExplicitSeq(t)))
+ }
+ case Range(min, max) =>
+ createRange(Tr(min), Tr(max))
+ case Append(e0, e1) =>
+ createAppendSeq(Tr(e0), Tr(e1))
+ case at@At(e0, e1) =>
+ FunctionApp("Seq#Index", List(Tr(e0), Tr(e1))) // of type: VarExpr(TrClass(e0.typ.parameters(0)))
+ case Drop(e0, e1) =>
+ Boogie.FunctionApp("Seq#Drop", List(Tr(e0), Tr(e1)))
+ case Take(e0, e1) =>
+ Boogie.FunctionApp("Seq#Take", List(Tr(e0), Tr(e1)))
+ case Length(e) =>
+ Boogie.FunctionApp("Seq#Length", List(Tr(e)))
+ case Eval(h, e) =>
+ val (evalHeap, evalMask, checks, assumptions) = fromEvalState(h);
+ val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask), currentClass);
+ evalEtran.Tr(e)
+ }
+
+ def translateForall(is: List[Variable], min: Expression, max: Expression, e: Expression): Expr = {
+ var assumption = true: Expr;
+ for(i <- is) {
+ assumption = assumption && (Tr(min) <= VarExpr(i.UniqueName) && VarExpr(i.UniqueName) < Tr(max));
+ }
+ new Boogie.Forall(is map { i=> Variable2BVar(i)}, Nil, assumption ==> Tr(e))
+ }
+
+ def ShaveOffOld(e: Expression): (Expression, boolean) = e match {
+ case Old(e) =>
+ val (f,o) = ShaveOffOld(e)
+ (f,true)
+ case _ => (e,false)
+ }
+ def IsMaxLockLit(e: Expression) = {
+ val (f,o) = ShaveOffOld(e)
+ f.isInstanceOf[MaxLockLiteral]
+ }
+
+ /**********************************************************************
+ ***************** INHALE/EXHALE *****************
+ **********************************************************************/
+
+ def Inhale(predicates: List[Expression], occasion: String, check: Boolean): List[Boogie.Stmt] = {
+ val (ihV, ih) = Boogie.NewBVar("inhaleHeap", theap, true)
+ Comment("inhale (" + occasion + ")") ::
+ BLocal(ihV) :: Boogie.Havoc(ih) ::
+ bassume(IsGoodInhaleState(ih, Heap, Mask)) ::
+ List.flatten (for (p <- predicates) yield Inhale(p,ih, check)) :::
+ bassume(IsGoodMask(Mask)) ::
+ bassume(wf(Heap, Mask)) ::
+ Comment("end inhale")
+ }
+
+ def InhaleFrom(predicates: List[Expression], occasion: String, check: Boolean, useHeap: Boogie.Expr): List[Boogie.Stmt] = {
+ val (ihV, ih) = Boogie.NewBVar("inhaleHeap", theap, true)
+ Comment("inhale (" + occasion + ")") ::
+ BLocal(ihV) :: Boogie.Assign(ih, useHeap) ::
+ bassume(IsGoodInhaleState(ih, Heap, Mask)) ::
+ List.flatten (for (p <- predicates) yield Inhale(p,ih, check)) :::
+ bassume(IsGoodMask(Mask)) ::
+ bassume(wf(Heap, Mask)) ::
+ Comment("end inhale")
+ }
+
+ def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean): List[Boogie.Stmt] = p match {
+ case pred@MemberAccess(e, p) if pred.isPredicate =>
+ val tmp = Access(pred, None);
+ tmp.pos = pred.pos;
+ Inhale(tmp, ih, check)
+ case acc@AccessAll(obj, perm) =>
+ obj.typ.Fields flatMap { f =>
+ val ma = MemberAccess(obj, f.id);
+ ma.f = f;
+ ma.pos = acc.pos;
+ val inhalee = Access(ma, perm);
+ inhalee.pos = acc.pos;
+ Inhale(inhalee, ih, check) }
+ case acc@RdAccessAll(obj, perm) =>
+ obj.typ.Fields flatMap { f =>
+ val ma = MemberAccess(obj, f.id);
+ ma.f = f;
+ ma.pos = acc.pos;
+ val inhalee = RdAccess(ma, perm);
+ inhalee.pos = acc.pos;
+ Inhale(inhalee, ih, check) }
+ case acc@Access(e,perm) =>
+ val trE = Tr(e.e)
+ val module = currentClass.module;
+ val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
+ (if(check) isDefined(e.e)(true)
+ // List(bassert(nonNull(trE), acc.pos, "The target of the acc predicate might be null."))
+ else Nil) :::
+ (perm match {
+ case None => List()
+ case Some(perm) =>
+ (if(check) isDefined(perm)(true) ::: bassert(Boogie.IntLiteral(0)<=Tr(perm), perm.pos, "Fraction might be negative.") ::
+ (if(! e.isPredicate) bassert(Tr(perm) <= Boogie.IntLiteral(100), perm.pos, "Fraction might exceed 100.") :: Nil else Nil) else Nil)
+ }) :::
+ bassume(nonNull(trE)) ::
+ MapUpdate(Heap, trE, memberName, Boogie.MapSelect(ih, trE, memberName)) ::
+ bassume(wf(Heap, Mask)) ::
+ (if(e.isPredicate && e.predicate.Parent.module.equals(currentClass.module)) List(bassume(Boogie.MapSelect(ih, trE, memberName) ==@ Heap)) else Nil) :::
+ (if(e.isPredicate) Nil else List(bassume(TypeInformation(Boogie.MapSelect(Heap, trE, memberName), e.f.typ)))) :::
+ (perm match {
+ case None => IncPermission(trE, memberName, 100)
+ case Some(perm) => IncPermission(trE, memberName, Tr(perm))
+ }) ::
+ bassume(IsGoodMask(Mask)) ::
+ bassume(IsGoodState(Boogie.MapSelect(ih, trE, memberName))) ::
+ bassume(wf(Heap, Mask)) ::
+ bassume(wf(ih, Mask))
+ case rdacc@RdAccess(e,perm) =>
+ val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
+ val trE = Tr(e.e)
+ val (dfP,p) = perm match {
+ case None => (List(), Boogie.IntLiteral(1))
+ case Some(None) => (List(), null)
+ case Some(Some(p)) => (isDefined(p)(true) ::: bassert(Boogie.IntLiteral(0)<=Tr(p), p.pos, "Number of epsilons might be negative."), Tr(p))
+ }
+ (if(check) { isDefined(e.e)(true) :::
+ // bassert(nonNull(trE), rdacc.pos, "The target of the rd predicate might be null.")
+ dfP } else Nil) :::
+ bassume(nonNull(trE)) ::
+ Boogie.MapUpdate(Heap, trE, memberName,
+ Boogie.MapSelect(ih, trE, memberName)) ::
+ bassume(Boogie.FunctionApp("wf", List(Heap, Mask))) ::
+ (if(e.isPredicate && e.predicate.Parent.module.equals(currentClass.module)) List(bassume(Boogie.MapSelect(ih, trE, memberName) ==@ Heap)) else Nil) :::
+ (if(e.isPredicate) Nil else List(bassume(TypeInformation(Boogie.MapSelect(Heap, trE, memberName), e.f.typ)))) :::
+ IncPermissionEpsilon(trE, memberName, p) ::
+ bassume(IsGoodMask(Mask)) ::
+ bassume(IsGoodState(Boogie.MapSelect(ih, trE, memberName))) ::
+ bassume(wf(Heap, Mask)) ::
+ bassume(wf(ih, Mask))
+ case Implies(e0,e1) =>
+ (if(check) isDefined(e0)(true) else Nil) :::
+ Boogie.If(Tr(e0), Inhale(e1, ih, check), Nil)
+ case IfThenElse(con, then, els) =>
+ (if(check) isDefined(con)(true) else Nil) :::
+ Boogie.If(Tr(con), Inhale(then, ih, check), Inhale(els, ih, check))
+ case And(e0,e1) =>
+ Inhale(e0, ih, check) ::: Inhale(e1, ih, check)
+ case holds@Holds(e) =>
+ val trE = Tr(e);
+ (if(check) isDefined(e)(true) :::
+ List(bassert(nonNull(trE), holds.pos, "The target of the holds predicate might be null.")) else Nil) :::
+ IncPermission(trE, "held", 100) :::
+ bassume(IsGoodMask(Mask)) ::
+ bassume(IsGoodState(Boogie.MapSelect(ih, trE, "held"))) ::
+ bassume(wf(Heap, Mask)) ::
+ bassume(wf(ih, Mask)) ::
+ Boogie.MapUpdate(Heap, trE, "held",
+ Boogie.MapSelect(ih, trE, "held")) ::
+ bassume(0 < Boogie.MapSelect(ih, trE, "held")) ::
+ bassume(! Boogie.MapSelect(ih, trE, "rdheld")) ::
+ bassume(wf(Heap, Mask)) ::
+ bassume(IsGoodMask(Mask)) ::
+ bassume(IsGoodState(Boogie.MapSelect(ih, trE, "held"))) ::
+ bassume(wf(Heap, Mask)) ::
+ bassume(wf(ih, Mask))
+ case Eval(h, e) =>
+ val (evalHeap, evalMask, checks, proofOrAssume) = fromEvalState(h);
+ val preGlobals = etran.FreshGlobals("eval")
+ val preEtran = new ExpressionTranslator(preGlobals map (v => new Boogie.VarExpr(v)), currentClass)
+ BLocal(preGlobals(0)) :: BLocal(preGlobals(1)) ::
+ (new VarExpr(preGlobals(1)) := ZeroMask) ::
+ // Should we start from ZeroMask instead of an arbitrary mask? In that case, assume submask(preEtran.Mask, evalMask); at the end!
+ (if(check) checks else Nil) :::
+ // havoc the held field when inhaling eval(o.release, ...)
+ (if(h.isInstanceOf[ReleaseState]) {
+ val (freshHeldV, freshHeld) = NewBVar("freshHeld", tint, true);
+ val obj = Tr(h.target());
+ List(BLocal(freshHeldV), bassume((0<Heap.select(obj, "held")) <==> (0<freshHeld)), (Heap.select(obj, "held") := freshHeld))
+ } else Nil) :::
+ bassume(IsGoodMask(preEtran.Mask)) ::
+ bassume(wf(preEtran.Heap, preEtran.Mask)) ::
+ bassume(proofOrAssume) ::
+ preEtran.Inhale(e, ih, check) :::
+ bassume(preEtran.Heap ==@ evalHeap) ::
+ bassume(submask(preEtran.Mask, evalMask))
+ case e => (if(check) isDefined(e)(true) else Nil) ::: bassume(Tr(e))
+ }
+
+ def Exhale(predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean): List[Boogie.Stmt] = {
+ val (emV, em) = NewBVar("exhaleMask", tmask, true)
+ Comment("begin exhale (" + occasion + ")") ::
+ BLocal(emV) :: (em := Mask) ::
+ (List.flatten (for (p <- predicates) yield Exhale(p._1, em, null, p._2, check))) :::
+ (Mask := em) ::
+ bassume(wf(Heap, Mask)) ::
+ Comment("end exhale")
+ }
+
+ def Exhale(p: Expression, em: Boogie.Expr, eh: Boogie.Expr, error: ErrorMessage, check: Boolean): List[Boogie.Stmt] = p match {
+ case pred@MemberAccess(e, p) if pred.isPredicate =>
+ val tmp = Access(pred, None);
+ tmp.pos = pred.pos;
+ Exhale(tmp, em , eh, error, check)
+ case acc@AccessAll(obj, perm) =>
+ obj.typ.Fields flatMap { f =>
+ val ma = MemberAccess(obj, f.id);
+ ma.f = f;
+ ma.pos = acc.pos;
+ val exhalee = Access(ma, perm);
+ exhalee.pos = acc.pos;
+ Exhale(exhalee, em, eh, error, check) }
+ case acc@RdAccessAll(obj, perm) =>
+ obj.typ.Fields flatMap { f =>
+ val ma = MemberAccess(obj, f.id);
+ ma.f = f;
+ ma.pos = acc.pos;
+ val exhalee = RdAccess(ma, perm);
+ exhalee.pos = acc.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
+ val (fraction, checkFraction) = perm match {
+ case None => (IntLiteral(100), Nil)
+ case Some(fr) => (fr, bassert(0<=Tr(fr), fr.pos, "Fraction might be negative.") :: (if(! e.isPredicate) bassert(Tr(fr)<=100, fr.pos, "Fraction might exceed 100.") :: Nil else Nil) ::: Nil)
+ }
+ val (fractionV, frac) = NewBVar("fraction", tint, true);
+ // check definedness
+ (if(check) isDefined(e.e)(true) :::
+ checkFraction :::
+ bassert(nonNull(Tr(e.e)), error.pos, error.message + " The target of the acc predicate at " + acc.pos + " might be null.") else Nil) :::
+ BLocal(fractionV) :: (frac := Tr(fraction)) ::
+ // if the mask does not contain sufficient permissions, try folding acc(e, fraction)
+ (if(e.isPredicate && autoFold && (!perm.isDefined || canTakeFractionOf(DefinitionOf(e.predicate)))) {
+ val inhaleTran = new ExpressionTranslator(List(Heap, em), currentClass);
+ val sourceVar = new Variable("fraction", new Type(IntClass));
+ val bplVar = Variable2BVar(sourceVar);
+ BLocal(bplVar) :: (VarExpr(sourceVar.UniqueName) := frac) ::
+ If(new MapSelect(em, Tr(e.e), memberName, "perm$R") < frac,
+ Exhale(if(perm.isDefined) FractionOf(SubstThis(DefinitionOf(e.predicate), e.e), new VariableExpr(sourceVar)) else SubstThis(DefinitionOf(e.predicate), e.e), em, eh, ErrorMessage(error.pos, error.message + " Automatic fold might fail."), false) :::
+ inhaleTran.Inhale(List(if(! perm.isDefined) Access(e, None) else Access(e, Some(new VariableExpr(sourceVar)))), "automatic fold", false)
+ , Nil) :: Nil}
+ else Nil) :::
+ // check that the necessary permissions are there and remove them from the mask
+ DecPermission(Tr(e.e), memberName, frac, em, error, acc.pos) :::
+ bassume(IsGoodMask(Mask)) ::
+ bassume(wf(Heap, Mask)) ::
+ bassume(wf(Heap, em))
+ case rd@RdAccess(e,perm) =>
+ val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
+ val (epsilonsV, eps) = NewBVar("epsilons", tint, true);
+ val (dfP, epsilons) = perm match {
+ case None => (List(), IntLiteral(1))
+ case Some(None) => (List(), null)
+ case Some(Some(p)) => (isDefined(p)(true) ::: List(bassert(0 <= Tr(p), error.pos, error.message + " The number of epsilons at " + rd.pos + " might be negative.")) , p)
+ }
+ // check definedness
+ (if(check) isDefined(e.e)(true) :::
+ bassert(nonNull(Tr(e.e)), error.pos, error.message + " The target of the rd predicate at " + rd.pos + " might be null.") ::
+ dfP else Nil) :::
+ BLocal(epsilonsV) :: (if(epsilons!=null) (eps := Tr(epsilons)) :: Nil else Nil) :::
+ // if the mask does not contain sufficient permissions, try folding rdacc(e, epsilons)
+ (if(e.isPredicate && autoFold && canTakeEpsilonsOf(DefinitionOf(e.predicate)) && epsilons!=null) {
+ val inhaleTran = new ExpressionTranslator(List(Heap, em), currentClass);
+ val sourceVar = new Variable("epsilons", new Type(IntClass));
+ val bplVar = Variable2BVar(sourceVar);
+ BLocal(bplVar) :: (VarExpr(sourceVar.UniqueName) := eps) ::
+ If(new MapSelect(em, Tr(e.e), memberName, "perm$N") < eps,
+ Exhale(EpsilonsOf(SubstThis(DefinitionOf(e.predicate), e.e), new VariableExpr(sourceVar)), em, eh, ErrorMessage(error.pos, error.message + " Automatic fold might fail."), false) :::
+ inhaleTran.Inhale(List(RdAccess(e, Some(Some(new VariableExpr(sourceVar))))), "automatic fold", false)
+ , Nil) :: Nil}
+ else Nil) :::
+ // check that the necessary permissions are there and remove them from the mask
+ DecPermissionEpsilon(Tr(e.e), memberName, if(epsilons != null) eps else null, em, error, rd.pos) :::
+ bassume(IsGoodMask(Mask)) ::
+ bassume(wf(Heap, Mask)) ::
+ bassume(wf(Heap, em))
+ case Implies(e0,e1) =>
+ (if(check) isDefined(e0)(true) else Nil) :::
+ Boogie.If(Tr(e0), Exhale(e1, em, eh, error, check), Nil)
+ case IfThenElse(con, then, els) =>
+ (if(check) isDefined(con)(true) else Nil) :::
+ Boogie.If(Tr(con), Exhale(then, em, eh, error, check), Exhale(els, em, eh, error, check))
+ case And(e0,e1) =>
+ Exhale(e0, em, eh, error, check) ::: Exhale(e1, em, eh, error, check)
+ case holds@Holds(e) =>
+ (if(check) isDefined(e)(true) :::
+ bassert(nonNull(Tr(e)), error.pos, error.message + " The target of the holds predicate at " + holds.pos + " might be null.") :: Nil else Nil) :::
+ bassert(HasFullPermission(Tr(e), "held", em), error.pos, error.message + " The current thread might not have full permission to the held field at " + holds.pos + ".") ::
+ bassert(0 < Boogie.MapSelect(Heap, Tr(e), "held"), error.pos, error.message + " The current thread might not hold lock at " + holds.pos + ".") ::
+ bassert(! Boogie.MapSelect(Heap, Tr(e), "rdheld"), error.pos, error.message + " The current thread might hold the read lock at " + holds.pos + ".") ::
+ SetNoPermission(Tr(e), "held", em) ::
+ bassume(IsGoodMask(Mask)) ::
+ bassume(wf(Heap, Mask)) ::
+ bassume(wf(Heap, em))
+ case Eval(h, e) =>
+ val (evalHeap, evalMask, checks, proofOrAssume) = fromEvalState(h);
+ val preGlobals = etran.FreshGlobals("eval")
+ val preEtran = new ExpressionTranslator(List(Boogie.VarExpr(preGlobals(0).id), Boogie.VarExpr(preGlobals(1).id)), currentClass);
+ BLocal(preGlobals(0)) :: (VarExpr(preGlobals(0).id) := evalHeap) ::
+ BLocal(preGlobals(1)) :: (VarExpr(preGlobals(1).id) := evalMask) ::
+ (if(check) checks else Nil) :::
+ bassume(IsGoodMask(preEtran.Mask)) ::
+ bassume(wf(preEtran.Heap, preEtran.Mask)) ::
+ bassert(proofOrAssume, p.pos, "Arguments for joinable might not match up.") ::
+ preEtran.Exhale(List((e, error)), "eval", check)
+ case e => (if(check) isDefined(e)(true) else Nil) ::: List(bassert(Tr(e), error.pos, error.message + " The expression at " + e.pos + " might not evaluate to true."))
+ }
+
+ def fromEvalState(h: EvalState): (Expr, Expr, List[Stmt], Expr) = {
+ h match {
+ case AcquireState(obj) =>
+ (AcquireHeap(Heap.select(Tr(obj), "held")), AcquireMask(Heap.select(Tr(obj), "held")), isDefined(obj)(true), true)
+ case ReleaseState(obj) =>
+ (LastSeenHeap(Heap.select(Tr(obj), "mu"), Heap.select(Tr(obj), "held")), LastSeenMask(Heap.select(Tr(obj), "mu"), Heap.select(Tr(obj), "held")), isDefined(obj)(true), true)
+ case CallState(token, obj, id, args) =>
+ val argsSeq = CallArgs(Heap.select(Tr(token), "joinable"));
+
+ var i : int = 0;
+ (CallHeap(Heap.select(Tr(token), "joinable")),
+ CallMask(Heap.select(Tr(token), "joinable")),
+ isDefined(token)(true) :::
+ isDefined(obj)(true) :::
+ (args flatMap { a => isDefined(a)(true)}) :::
+ bassert(CanRead(Tr(token), "joinable"), obj.pos, "Joinable field of the token might not be readable.") ::
+ bassert(Heap.select(Tr(token), "joinable") !=@ 0, obj.pos, "Token might not be active."),
+ (new MapSelect(argsSeq, 0) ==@ Tr(obj) ) &&
+ (((args zip (1 until args.length+1).toList) map { a => new MapSelect(argsSeq, a._2) ==@ Tr(a._1)}).foldLeft(true: Expr){ (a: Expr, b: Expr) => a && b})
+ )
+ }
+ }
+
+ // permissions
+
+ def CanRead(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = new Boogie.FunctionApp("CanRead", Mask, obj, field)
+ def CanRead(obj: Boogie.Expr, field: String): Boogie.Expr = CanRead(obj, new Boogie.VarExpr(field))
+ def CanWrite(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = new Boogie.FunctionApp("CanWrite", Mask, obj, field)
+ def CanWrite(obj: Boogie.Expr, field: String): Boogie.Expr = CanWrite(obj, new Boogie.VarExpr(field))
+ def HasNoPermission(obj: Boogie.Expr, field: String) =
+ (new Boogie.MapSelect(Mask, obj, field, "perm$R") ==@ Boogie.IntLiteral(0)) &&
+ (new Boogie.MapSelect(Mask, obj, field, "perm$N") ==@ Boogie.IntLiteral(0))
+ def SetNoPermission(obj: Boogie.Expr, field: String, mask: Boogie.Expr) =
+ Boogie.Assign(Boogie.MapSelect(mask, obj, field), Boogie.VarExpr("Permission$Zero"))
+ def HasFullPermission(obj: Boogie.Expr, field: String, mask: Boogie.Expr) =
+ (new Boogie.MapSelect(mask, obj, field, "perm$R") ==@ Boogie.IntLiteral(100)) &&
+ (new Boogie.MapSelect(mask, obj, field, "perm$N") ==@ Boogie.IntLiteral(0))
+ def SetFullPermission(obj: Boogie.Expr, field: String) =
+ Boogie.Assign(Boogie.MapSelect(Mask, obj, field), Boogie.VarExpr("Permission$Full"))
+
+ def IncPermission(obj: Boogie.Expr, field: String, howMuch: Boogie.Expr) =
+ MapUpdate3(Mask, obj, field, "perm$R", new Boogie.MapSelect(Mask, obj, field, "perm$R") + howMuch)
+ def IncPermissionEpsilon(obj: Boogie.Expr, field: String, epsilons: Boogie.Expr) =
+ if (epsilons != null) {
+ val g = (new Boogie.MapSelect(Mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$MinusInfinity")) &&
+ (new Boogie.MapSelect(Mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$PlusInfinity"))
+ Boogie.If(g,
+ MapUpdate3(Mask, obj, field, "perm$N", new Boogie.MapSelect(Mask, obj, field, "perm$N") + epsilons) ::
+ bassume(Boogie.FunctionApp("wf", List(Heap, Mask))) :: Nil
+ , Nil)
+ } else {
+ val g = (new Boogie.MapSelect(Mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$MinusInfinity"))
+ Boogie.If(g, MapUpdate3(Mask, obj, field, "perm$N", Boogie.VarExpr("Permission$PlusInfinity")), Nil)
+ }
+
+ def DecPermission(obj: Boogie.Expr, field: String, howMuch: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position) = {
+ val xyz: Boogie.Expr = new Boogie.MapSelect(mask, obj, field, "perm$R")
+ bassert(howMuch <= xyz, error.pos, error.message + " Insufficient fraction at " + pos + " for " + field + ".") ::
+ MapUpdate3(mask, obj, field, "perm$R", new Boogie.MapSelect(mask, obj, field, "perm$R") - howMuch)
+ }
+ def DecPermissionEpsilon(obj: Boogie.Expr, field: String, epsilons: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position) =
+ if (epsilons != null) {
+ val g = (new Boogie.MapSelect(mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$MinusInfinity")) &&
+ (new Boogie.MapSelect(mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$PlusInfinity"))
+ val xyz = new Boogie.MapSelect(mask, obj, field, "perm$N")
+ bassert((new Boogie.MapSelect(mask, obj, field, "perm$R") ==@ Boogie.IntLiteral(0)) ==> (epsilons <= xyz), error.pos, error.message + " Insufficient epsilons at " + pos + " for " + field + ".") ::
+ Boogie.If(g,
+ MapUpdate3(mask, obj, field, "perm$N", new Boogie.MapSelect(mask, obj, field, "perm$N") - epsilons) ::
+ bassume(Boogie.FunctionApp("wf", List(Heap, Mask))) :: Nil
+ , Nil)
+ } else {
+ val g = (new Boogie.MapSelect(mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$PlusInfinity"))
+ bassert((new Boogie.MapSelect(mask, obj, field, "perm$R") ==@ Boogie.IntLiteral(0)) ==>
+ (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
+ // m[a,b][c] := rhs
+ // m[a,b] := map[a,b][c := rhs]
+ val m01 = Boogie.MapSelect(m, arg0, arg1)
+ Boogie.Assign(m01, Boogie.MapStore(m01, arg2, rhs))
+ }
+
+ def DecPerm(m: Expr, e: Expr, f: Expr, i: Expr) = FunctionApp("DecPerm", List(m, e, f, i))
+ def DecEpsilons(m: Expr, e: Expr, f: Expr, i: Expr) = FunctionApp("DecEpsilons", List(m, e, f, i))
+ def IncPerm(m: Expr, e: Expr, f: Expr, i: Expr) = FunctionApp("IncPerm", List(m, e, f, i))
+ def IncEpsilons(m: Expr, e: Expr, f: Expr, i: Expr) = FunctionApp("IncEpsilons", List(m, e, f, i))
+
+
+ def MaxLockIsBelowX(x: Boogie.Expr) = { // maxlock << x
+ val (oV, o) = Boogie.NewBVar("o", tref, false)
+ new Boogie.Forall(oV,
+ (isHeldInHeap(o, Heap)) ==>
+ new Boogie.FunctionApp("MuBelow", Boogie.MapSelect(Heap, o, "mu"), x))
+ }
+ def MaxLockIsAboveX(x: Boogie.Expr) = { // x << maxlock
+ val (oV, o) = Boogie.NewBVar("o", tref, false)
+ new Boogie.Exists(oV,
+ (isHeldInHeap(o, Heap)) &&
+ new Boogie.FunctionApp("MuBelow", x, Boogie.MapSelect(Heap, o, "mu")))
+ }
+ def MaxLockEqualsX(x: Boogie.Expr) = { // maxlock == o.mu
+ // Note: Instead of the existential below, we could generate a nicer expression if we knew that
+ // x has the form y.mu--then, we'd replace the existential with y.held. Another possibility
+ // would be if we had an inverse of .mu (such an inverse exists, but we're not encoding it).
+// val (oV, o) = Boogie.NewBVar("o", tref, false)
+ //new Boogie.Exists(oV,
+ // (isHeldInHeap(o, Heap)) && (Boogie.MapSelect(Heap, o, "mu") ==@ x)) &&
+ /*isHeldInHeap(x, Heap) &&*/ IsHighestLock(x)
+ }
+ def IsHighestLock(x: Boogie.Expr) = {
+ // (forall r :: r.held ==> r.mu << x || r.mu == x)
+ val (rV, r) = Boogie.NewBVar("r", tref, false)
+ new Boogie.Forall(rV,
+ (isHeldInHeap(r, Heap)) ==>
+ (new Boogie.FunctionApp("MuBelow", MapSelect(Heap, r, "mu"), x) ||
+ (Boogie.MapSelect(Heap, r, "mu") ==@ x)))
+ }
+ def MaxLockPreserved = { // old(maxlock) == maxlock
+ // I don't know what the best encoding of this conding is, so I'll try a disjunction.
+ // Disjunct b0 is easier to prove, but it is stronger than b1.
+
+ // (forall r: ref ::
+ // old(Heap)[r,held] == Heap[r,held] &&
+ // (Heap[r,held] ==> old(Heap)[r,mu] == Heap[r,mu]))
+ val (rV, r) = Boogie.NewBVar("r", tref, false)
+ val b0 = new Boogie.Forall(rV,
+ ((0 < Boogie.MapSelect(oldEtran.Heap, r, "held")) ==@
+ (0 < Boogie.MapSelect(Heap, r, "held"))) &&
+ ((0 < Boogie.MapSelect(Heap, r, "held")) ==>
+ (Boogie.MapSelect(oldEtran.Heap, r, "mu") ==@
+ Boogie.MapSelect(Heap, r, "mu"))))
+
+ // (forall o, p ::
+ // old(o.held) && (forall r :: old(r.held) ==> old(r.mu) << old(o.mu) || old(r.mu)==old(o.mu)) &&
+ // p.held && (forall r :: r.held ==> r.mu << p.mu || r.mu == p.mu )
+ // ==>
+ // old(o.mu) == p.mu)
+ val (oV, o) = Boogie.NewBVar("o", tref, false)
+ val (pV, p) = Boogie.NewBVar("p", tref, false)
+ val b1 = new Boogie.Forall(List(oV,pV), List(),
+ ((0 < Boogie.MapSelect(oldEtran.Heap, o, "held")) &&
+ oldEtran.IsHighestLock(Boogie.MapSelect(oldEtran.Heap, o, "mu")) &&
+ (0 < Boogie.MapSelect(Heap, p, "held")) &&
+ IsHighestLock(Boogie.MapSelect(Heap, p, "mu")))
+ ==>
+ (Boogie.MapSelect(oldEtran.Heap, o, "mu") ==@ Boogie.MapSelect(Heap, p, "mu")))
+ b0 || b1
+ }
+ def TemporalMaxLockComparison(e0: ExpressionTranslator, e1: ExpressionTranslator) = { // e0(maxlock) << e1(maxlock)
+ // (exists o ::
+ // e1(o.held) &&
+ // (forall r :: e0(r.held) ==> e0(r.mu) << e1(o.mu)))
+ val (oV, o) = Boogie.NewBVar("o", tref, false)
+ new Boogie.Exists(oV,
+ (0 < Boogie.MapSelect(e0.Heap, o, "held")) &&
+ e0.MaxLockIsBelowX(Boogie.MapSelect(e1.Heap, o, "mu")))
+ }
+
+ def fractionOk(expr: Expression) = {
+ bassert(0<=Tr(expr), expr.pos, "Fraction might be negative.") ::
+ bassert(Tr(expr) <= 100, expr.pos, "Fraction might exceed 100.")
+ }
+}
+object S_ExpressionTranslator {
+ val Globals = {
+ ("Heap", theap) ::
+ ("Mask", tmask) ::
+ Nil
+ }
+}
+
+
+ // implicit
+ implicit def string2VarExpr(s: String) = VarExpr(s)
+ implicit def expression2Expr(e: Expression) = etran.Tr(e)
+ implicit def field2Expr(f: Field) = VarExpr(f.FullName)
+
+ // prelude
+
+ def ModuleType = NamedType("ModuleName");
+ def ModuleName(cl: Class) = "module#" + cl.module.id;
+ def TypeName = NamedType("TypeName");
+ def FieldType(tp: BType) = IndexedType("Field", tp);
+ def bassert(e: Expr, pos: Position, msg: String) = {
+ val result = Boogie.Assert(e); result.pos = pos; result.message = msg; result
+ }
+ def bassume(e: Expr) = Boogie.Assume(e)
+ def BLocal(id: String, tp: BType) = new Boogie.LocalVar(id, tp)
+ def BLocal(x: Boogie.BVar) = Boogie.LocalVar(x)
+ def tArgSeq = NamedType("ArgSeq");
+ def tref = NamedType("ref");
+ def tbool = NamedType("bool");
+ def tmu = NamedType("Mu");
+ def tint = NamedType("int");
+ def tseq(arg: BType) = IndexedType("Seq", arg)
+ def theap = NamedType("HeapType");
+ def tmask = NamedType("MaskType");
+ def ZeroMask = VarExpr("ZeroMask");
+ def HeapName = "Heap";
+ def MaskName = "Mask";
+ def Heap = VarExpr(HeapName);
+ def Mask = VarExpr(MaskName);
+ def GlobalNames = List(HeapName, MaskName);
+ def CanAssumeFunctionDefs = VarExpr("CanAssumeFunctionDefs");
+ def CurrentModule = VarExpr("CurrentModule");
+ def IsGoodState(e: Expr) = FunctionApp("IsGoodState", List(e));
+ def dtype(e: Expr) = FunctionApp("dtype", List(e))
+ def functionName(f: Function) = "#" + f.FullName;
+ 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 AcquireHeap(heldBit: Expr) = FunctionApp("Acquire$Heap", List(heldBit))
+ def AcquireMask(heldBit: Expr) = FunctionApp("Acquire$Mask", List(heldBit))
+ def CallHeap(joinableBit: Expr) = FunctionApp("Call$Heap", List(joinableBit))
+ def CallMask(joinableBit: Expr) = FunctionApp("Call$Mask", List(joinableBit))
+ def CallArgs(joinableBit: Expr) = FunctionApp("Call$Args", List(joinableBit))
+ def submask(m1: Expr, m2: Expr) = FunctionApp("submask", List(m1, m2))
+
+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))
+ def isHeldInHeap(e: Expr, h: Expr) = 0 < h.select(e, "held")
+ def NonEmptyMask(m: Expr) = ! FunctionApp("EmptyMask", List(m))
+ def NonPredicateField(f: String) = FunctionApp("NonPredicateField", List(VarExpr(f)))
+ def PredicateField(f: String) = FunctionApp("PredicateField", List(VarExpr(f)))
+ def createEmptySeq = FunctionApp("Seq#Empty", List())
+ def createSingletonSeq(e: Expr) = FunctionApp("Seq#Singleton", List(e))
+ def createAppendSeq(a: Expr, b: Expr) = FunctionApp("Seq#Append", List(a, b))
+ 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(tp: Type): BType = {
+ val cl = tp.typ;
+ 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(new Type(cl.asInstanceOf[SeqClass].parameter)))
+ } else {
+ assert(false); 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, Boogie.ClassType(v.t.typ))
+ def Variable2BVarWhere(v: Variable) = NewBVarWhere(v.UniqueName, v.t)
+ def NewBVarWhere(id: String, tp: Type) = {
+ new Boogie.BVar(id, Boogie.ClassType(tp.typ)){
+ override val where = TypeInformation(new Boogie.VarExpr(id), tp) }
+ }
+
+ // scale an expression by a fraction
+ def FractionOf(expr: Expression, fraction: Expression) : Expression = {
+ val result = expr match {
+ case Access(e, None) => Access(e, Some(fraction))
+ case And(lhs, rhs) => And(FractionOf(lhs, fraction), FractionOf(rhs, fraction))
+ case _ if ! expr.isInstanceOf[PermissionExpr] => expr
+ case _ => throw new Exception(" " + expr.pos + ": Scaling non-full permissions is not supported yet." + expr);
+ }
+ result.pos = expr.pos;
+ result
+ }
+
+ def canTakeFractionOf(expr: Expression): Boolean = {
+ expr match {
+ case Access(e, None) => true
+ case And(lhs, rhs) => canTakeFractionOf(lhs) && canTakeFractionOf(rhs)
+ case _ if ! expr.isInstanceOf[PermissionExpr] => true
+ case _ => false
+ }
+ }
+
+ // scale an expression by a number of epsilons
+ def EpsilonsOf(expr: Expression, nbEpsilons: Expression) : Expression = {
+ val result = expr match {
+ case Access(e, _) => RdAccess(e, Some(Some(nbEpsilons)))
+ case And(lhs, rhs) => And(FractionOf(lhs, nbEpsilons), FractionOf(rhs, nbEpsilons))
+ case _ if ! expr.isInstanceOf[PermissionExpr] => expr
+ case _ => throw new Exception(" " + expr.pos + ": Scaling non-full permissions is not supported yet." + expr);
+ }
+ result.pos = expr.pos;
+ result
+ }
+
+ def canTakeEpsilonsOf(expr: Expression): Boolean = {
+ expr match {
+ case Access(e, _) => true
+ case And(lhs, rhs) => canTakeEpsilonsOf(lhs) && canTakeEpsilonsOf(rhs)
+ case _ if ! expr.isInstanceOf[PermissionExpr] => true
+ case _ => false
+ }
+ }
+
+ def TrType(cl: Class) = Boogie.VarExpr(cl.id + "#t")
+
+ def TypeInformation(e: Boogie.Expr, t: Type): Boogie.Expr = {
+ if (t.typ.IsRef) {
+ (e ==@ Boogie.Null()) || (new Boogie.FunctionApp("dtype", e) ==@ TrType(t.typ))
+ } else {
+ true
+ }
+ }
+
+ def Version(expr: Expression, etran: ExpressionTranslator): Boogie.Expr =
+ {
+ expr match{
+ case pred@MemberAccess(e, p) if pred.isPredicate =>
+ Version(Access(pred, None), etran)
+ case acc@Access(e,perm) =>
+ val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
+ Boogie.MapSelect(etran.Heap, etran.Tr(e.e), memberName)
+ case rd@RdAccess(e,perm) =>
+ val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
+ Boogie.MapSelect(etran.Heap, etran.Tr(e.e), memberName)
+ case Implies(e0,e1) =>
+ Boogie.Ite(etran.Tr(e0), Version(e1, etran), 0)
+ case And(e0,e1) =>
+ Boogie.FunctionApp("combine", List(Version(e0, etran), Version(e1, etran)))
+ case IfThenElse(con, then, els) =>
+ Boogie.Ite(etran.Tr(con), Version(then, etran), Version(els, etran))
+ case e => Boogie.VarExpr("nostate")
+ }
+ }
+ def FieldTp(f: Field): String = {
+ f match {
+ case SpecialField("mu", _) => "Mu"
+ case SpecialField("held", _) => "int"
+ case SpecialField("rdheld", _) => "bool"
+ case SpecialField("joinable", _) => "int"
+ case f: Field => TrClass(f.typ.typ)
+ }
+ }
+
+ def TrClass(tp: Class): String = {
+ tp.id match {
+ case "int" => "int"
+ case "bool" => "bool"
+ case "$Mu" => "Mu"
+ case _ => if(tp.IsSeq) "seq" else "ref"
+ }
+ }
+ def Preconditions(spec: List[Specification]): List[Expression] = {
+ val result = spec flatMap ( s => s match {
+ case Precondition(e) => List(e)
+ case _ => Nil });
+ if(autoMagic) {
+ automagic(result.foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b)}), Nil)._1 ::: result
+ } else {
+ result
+ }
+ }
+ def Postconditions(spec: List[Specification]): List[Expression] = {
+ val result = spec flatMap ( s => s match {
+ case Postcondition(e) => List(e)
+ case _ => Nil })
+ if(autoMagic) {
+ automagic(result.foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b)}), Nil)._1 ::: result
+ } else {
+ result
+ }
+ }
+
+ def automagic(expr: Expression, handled: List[Expression]): (/*assumptions*/ List[Expression], /*newHandled*/List[Expression]) = {
+ def isHandled(e: Expression) = handled exists { ex => ex.equals(e) }
+ expr match {
+ case ma@MemberAccess(obj, f) =>
+ val (assumptions, handled1) = automagic(obj, handled);
+ if(isHandled(ma)) {
+ (assumptions, handled1)
+ } else {
+ if(ma.isPredicate){
+ // assumption: obj!=null
+ (assumptions ::: Neq(obj, NullLiteral()) :: Nil, handled1 + ma)
+ } else {
+ // assumption: obj!=null && acc(obj, f)
+ (assumptions ::: Neq(obj, NullLiteral()) :: Access(ma, None) :: Nil, handled1 + ma)
+ }
+ }
+ case Access(ma@MemberAccess(obj, f), perm) =>
+ val (assumptions, handled1) = automagic(obj, handled + ma);
+ perm match {
+ case None => (assumptions, handled1);
+ case Some(fraction) => val result = automagic(fraction, handled1); (assumptions ::: result._1, result._2)
+ }
+ case RdAccess(ma@MemberAccess(obj, f), perm) =>
+ val (assumptions, handled1) = automagic(obj, handled + ma);
+ perm match {
+ case None => (assumptions, handled1);
+ case Some(None) => (assumptions, handled1);
+ case Some(Some(epsilon)) => val result = automagic(epsilon, handled1); (assumptions ::: result._1, result._2)
+ }
+ case AccessAll(obj, perm) =>
+ automagic(obj, handled)
+ case RdAccessAll(obj, perm) =>
+ automagic(obj, handled)
+ case Holds(e) =>
+ automagic(e, handled)
+ case RdHolds(e) =>
+ automagic(e, handled)
+ case a: Assigned =>
+ (Nil, handled)
+ case Old(e) =>
+ (Nil, handled) // ??
+ case IfThenElse(con, then, els) =>
+ val (assumptions, handled1) = automagic(con, handled);
+ val (assumptions2, handled2) = automagic(then, handled1);
+ val result = automagic(els, handled2);
+ (assumptions ::: assumptions2 ::: result._1, result._2)
+ case Not(e) =>
+ automagic(e, handled)
+ case func@FunctionApplication(obj, id, args) =>
+ var assumption = Nil: List[Expression];
+ var newHandled = handled;
+ for(a <- obj :: args) {
+ val (ass, hd) = automagic(a, handled);
+ assumption = assumption ::: ass;
+ newHandled = hd;
+ }
+ (assumption, newHandled)
+ case uf@Unfolding(_, e) =>
+ (Nil, handled)
+ case bin: BinaryExpr =>
+ val (assumptions, handled1) = automagic(bin.E0, handled);
+ val result = automagic(bin.E1, handled1);
+ (assumptions ::: result._1, result._2)
+ case q@Forall(is, Range(min, max), e) =>
+ (Nil, handled)
+ case q@Forall(is, seq, e) =>
+ (Nil, handled)
+ case EmptySeq(t) =>
+ (Nil, handled)
+ case ExplicitSeq(es) =>
+ var assumption = Nil: List[Expression];
+ var newHandled = handled;
+ for(a <- es) {
+ val (ass, hd) = automagic(a, handled);
+ assumption = assumption ::: ass;
+ newHandled = hd;
+ }
+ (assumption, newHandled)
+ case Range(min, max) =>
+ val (assumptions, handled1) = automagic(min, handled);
+ val result = automagic(max, handled1);
+ (assumptions ::: result._1, result._2)
+ case Length(e) =>
+ automagic(e, handled)
+ case Eval(h, e) =>
+ (Nil, handled)
+ case _ => (Nil, handled)
+ }
+ }
+
+ def DefinitionOf(predicate: Predicate): Expression = {
+ if(autoMagic) {
+ And(automagic(predicate.definition, Nil)._1.foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b)}), predicate.definition)
+ } else {
+ predicate.definition
+ }
+ }
+
+ def LockChanges(spec: List[Specification]): List[Expression] = {
+ spec flatMap ( s => s match {
+ case LockChange(ee) => ee
+ case _ => Nil })
+ }
+
+ def SubstRd(e: Expression): Expression = e match {
+ case Access(e,_) =>
+ val r = RdAccess(e,None); r.typ = BoolClass; r
+ case e: RdAccess => e
+ case Implies(e0,e1) =>
+ val r = Implies(e0, SubstRd(e1)); r.typ = BoolClass; r
+ 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 = {
+ e match {
+ case pred@MemberAccess(o, f) if pred.isPredicate && o.isInstanceOf[ThisExpr] =>
+ SubstThis(DefinitionOf(pred.predicate), o)
+ case Access(pred@MemberAccess(o, f), p) if pred.isPredicate && o.isInstanceOf[ThisExpr] =>
+ p match {
+ case None => SubstThis(DefinitionOf(pred.predicate), o)
+ case Some(p) => FractionOf(SubstThis(DefinitionOf(pred.predicate), o), p)
+ }
+ case RdAccess(pred@MemberAccess(o, f), p) if pred.isPredicate && o.isInstanceOf[ThisExpr] =>
+ p match {
+ case None => EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), o), IntLiteral(1))
+ case Some(None) => throw new Exception("not supported yet")
+ case Some(Some(p)) => EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), o), p)
+ }
+ case func@FunctionApplication(obj: ThisExpr, name, args) if 2<=TranslationOptions.defaults =>
+ SubstThisAndVars(func.f.definition, obj, func.f.ins, args)
+ case _ => manipulate(e, {ex => unfoldPred(ex)})
+ }
+ }
+ unfoldPred(expr)
+ }
+
+ // needed to do a _simultaneous_ substitution!
+ def SubstThisAndVars(expr: Expression, thisReplacement: Expression, vs: List[Variable], xs: List[Expression]): Expression = {
+ def replace(e: Expression): Expression = {
+ e match {
+ case _: ThisExpr => thisReplacement
+ case e: VariableExpr =>
+ for ((v,x) <- vs zip xs if v == e.v) { return x }
+ e
+ case q@Forall(is, seq, e) =>
+ val sub = vs zip xs filter { xv => is forall { variable => ! variable.id.equals(xv._1)}};
+ val result = Forall(is, SubstThisAndVars(seq, thisReplacement, vs, xs), SubstThisAndVars(e, thisReplacement, sub map { x => x._1}, sub map { x => x._2}));
+ result.variables = q.variables;
+ result
+ case _ => manipulate(e, {ex => replace(ex)})
+ }
+ }
+ replace(expr)
+ }
+
+ def SubstThis(expr: Expression, x: Expression): Expression = {
+ def replaceThis(e: Expression): Expression = {
+ e match {
+ case _: ThisExpr => x
+ case _ => manipulate(e, {ex => replaceThis(ex)})
+ }
+ }
+ replaceThis(expr)
+ }
+
+ def SubstResult(expr: Expression, x: Expression): Expression = {
+ def replaceThis(e: Expression): Expression = {
+ e match {
+ case _: Result => x
+ case _ => manipulate(e, {ex => replaceThis(ex)})
+ }
+ }
+ replaceThis(expr)
+ }
+
+ def SubstVars(expr: Expression, vs: List[Variable], xs: List[Expression]): Expression = {
+ def replaceThis(e: Expression): Expression = {
+ e match {
+ case e: VariableExpr =>
+ for ((v,x) <- vs zip xs if v == e.v) { return x }
+ e
+ case q@Forall(is, seq, e) =>
+ val sub = vs zip xs filter { xv => is forall { variable => ! variable.id.equals(xv._1)}};
+ val result = Forall(is, SubstVars(seq, vs, xs), SubstVars(e, sub map { x => x._1}, sub map { x => x._2}));
+ result.variables = q.variables;
+ result
+ case _ => manipulate(e, {ex => replaceThis(ex)})
+ }
+ }
+ replaceThis(expr)
+ }
+
+ def manipulate(expr: Expression, func: Expression => Expression): Expression = {
+ val result = expr match {
+ case e: Literal => expr
+ case _:ThisExpr => expr
+ case _:Result => expr
+ case e:VariableExpr => expr
+ case acc@MemberAccess(e,f) =>
+ val g = MemberAccess(func(e), f); g.f = acc.f; g.predicate = acc.predicate; g.isPredicate = acc.isPredicate; g
+ case Access(e, perm) =>
+ Access(func(e).asInstanceOf[MemberAccess],
+ 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 })
+ 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 })
+ case Holds(e) => Holds(func(e))
+ case RdHolds(e) => RdHolds(func(e))
+ case e: Assigned => e
+ case Old(e) => Old(func(e))
+ case IfThenElse(con, then, els) => IfThenElse(func(con), func(then), func(els))
+ case Not(e) => Not(func(e))
+ 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))
+ 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))
+ case Or(e0,e1) => Or(func(e0), func(e1))
+ case Eq(e0,e1) => Eq(func(e0), func(e1))
+ case Neq(e0,e1) => Neq(func(e0), func(e1))
+ case Less(e0,e1) => Less(func(e0), func(e1))
+ case AtMost(e0,e1) => AtMost(func(e0), func(e1))
+ case AtLeast(e0,e1) => AtLeast(func(e0), func(e1))
+ case Greater(e0,e1) => Greater(func(e0), func(e1))
+ case LockBelow(e0,e1) => LockBelow(func(e0), func(e1))
+ case Plus(e0,e1) => Plus(func(e0), func(e1))
+ case Minus(e0,e1) => Minus(func(e0), func(e1))
+ case Times(e0,e1) => Times(func(e0), func(e1))
+ case Div(e0,e1) => Div(func(e0), func(e1))
+ case Mod(e0,e1) => Mod(func(e0), func(e1))
+ case forall@Forall(i, seq, e) => val result = Forall(i, func(seq), func(e)); result.variables = forall.variables; result
+ case ExplicitSeq(es) =>
+ ExplicitSeq(es map { e => func(e) })
+ case Range(min, max)=>
+ Range(func(min), func(max))
+ case Append(e0, e1) =>
+ Append(func(e0), func(e1))
+ case At(e0, e1) =>
+ At(func(e0), func(e1))
+ case Drop(e0, e1) =>
+ Drop(func(e0), func(e1))
+ case Take(e0, e1) =>
+ Take(func(e0), func(e1))
+ case Length(e) =>
+ Length(func(e))
+ case Eval(h, e) =>
+ Eval(h match {
+ case AcquireState(obj) => AcquireState(func(obj))
+ case ReleaseState(obj) => ReleaseState(func(obj))
+ case CallState(token, obj, i, args) => CallState(func(token), func(obj), i, args map { a => func(a)})
+ }, func(e))
+ }
+ if(result.typ == null) {
+ result.typ = expr.typ;
+ }
+ result.pos = expr.pos
+ result
+ }
+
+}
|