summaryrefslogtreecommitdiff
path: root/Chalice/src
diff options
context:
space:
mode:
authorGravatar kyessenov <unknown>2010-08-02 08:18:36 +0000
committerGravatar kyessenov <unknown>2010-08-02 08:18:36 +0000
commit95769d85da74b3eb44d239fdc8c3705250bc027c (patch)
treec46cedb3834065a8cb55eaa3e326d64d5edc9344 /Chalice/src
parent1679c064cdb5c667d9f8e46eaac58a65c66d8b11 (diff)
Chalice:
* added quantifiers over any type (forall i: int :: i + 1 == i + 1) * cleaned up AST transformation code; organized one transform operation that should preserve source positions -- it was very annoying to see assertions with lost source positions * added a desugar method that simplifies Chalice AST by unrolling a few constructs -- maybe useful in the future to quickly add a syntactic sugar
Diffstat (limited to 'Chalice/src')
-rw-r--r--Chalice/src/Ast.scala237
-rw-r--r--Chalice/src/Boogie.scala17
-rw-r--r--Chalice/src/ChaliceToCSharp.scala2
-rw-r--r--Chalice/src/Parser.scala53
-rw-r--r--Chalice/src/PrettyPrinter.scala12
-rw-r--r--Chalice/src/Resolver.scala134
-rw-r--r--Chalice/src/Translator.scala428
7 files changed, 446 insertions, 437 deletions
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 25bfb975..0414285d 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -4,6 +4,7 @@
//
//-----------------------------------------------------------------------------
import scala.util.parsing.input.Position
+import scala.util.parsing.input.NoPosition
import scala.util.parsing.input.Positional
trait ASTNode extends Positional
@@ -124,10 +125,8 @@ sealed abstract class NamedMember(id: String) extends Member {
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
+case class Field(id: String, typ: Type, isGhost: Boolean) extends NamedMember(id)
+case class SpecialField(name: String, tp: Type) extends Field(name, tp, false) { // 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)
@@ -146,12 +145,12 @@ class Variable(name: String, typ: Type) extends ASTNode {
val IsGhost: Boolean = false
val IsImmutable: Boolean = false
val UniqueName = {
- val n = S_Variable.VariableCount
- S_Variable.VariableCount = S_Variable.VariableCount + 1
+ val n = Variable.VariableCount
+ Variable.VariableCount = Variable.VariableCount + 1
name + "#" + n
}
}
-object S_Variable { var VariableCount = 0 }
+object Variable { var VariableCount = 0 }
class ImmutableVariable(id: String, t: Type) extends Variable(id, t) {
override val IsImmutable: Boolean = true
}
@@ -234,7 +233,9 @@ case class NewRhs(id: String, initialization: List[Init], lowerBounds: List[Expr
case class Init(id: String, e: Expression) extends ASTNode {
var f: Field = null;
}
-sealed abstract class Expression extends RValue
+sealed abstract class Expression extends RValue {
+ def transform(f: Expression => Option[Expression]) = AST.transform(this, f)
+}
sealed abstract class Literal extends Expression
case class IntLiteral(n: Int) extends Literal
case class BoolLiteral(b: Boolean) extends Literal
@@ -273,14 +274,12 @@ case class Epsilons(n: Expression) extends Read // Some(Some(n))
sealed abstract class PermissionExpr(perm: Permission) extends Expression
sealed abstract class WildCardPermission(perm: Permission) extends PermissionExpr(perm)
-case class Access(e: MemberAccess, perm: Permission) extends PermissionExpr(perm) {
- def getMemberAccess = e : MemberAccess;
-}
+case class Access(ma: MemberAccess, perm: Permission) extends PermissionExpr(perm)
case class AccessAll(obj: Expression, perm: Permission) extends WildCardPermission(perm)
case class AccessSeq(s: Expression, f: Option[MemberAccess], perm: Permission) extends WildCardPermission(perm)
case class Credit(e: Expression, n: Option[Expression]) extends Expression {
- def N = n match { case None => IntLiteral(1) case Some(n) => n }
+ val N = n match { case None => IntLiteral(1) case Some(n) => n }
}
case class Holds(e: Expression) extends Expression
@@ -295,10 +294,10 @@ case class FunctionApplication(obj: Expression, id: String, args: List[Expressio
}
case class Unfolding(pred: Access, 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 E0 = e0
+ val E1 = e1
+ val ExpectedLhsType: Class = BoolClass // sometimes undefined
+ val ExpectedRhsType: Class = BoolClass // sometimes undefined
val ResultType: Class = BoolClass
val OpName: String
}
@@ -315,8 +314,8 @@ 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 ExpectedLhsType = IntClass
+ override val ExpectedRhsType = IntClass
override val ResultType = IntClass
}
case class Plus(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
@@ -335,12 +334,12 @@ 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
+ override val ExpectedLhsType = IntClass
+ override val 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")
+ override val ExpectedLhsType = null;
+ override val ExpectedRhsType = null;
}
case class Eq(e0: Expression, e1: Expression) extends EqualityCompareExpr(e0,e1) {
override val OpName = "=="
@@ -361,23 +360,24 @@ 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 ExpectedLhsType = null;
+ override val ExpectedRhsType = null;
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"
-}
-case class Exists(is: List[String], seq: Expression, e: Expression) extends Quantification(is, seq, e) {
- override def Quantor = "exists"
-}
+
+// quantifiers
+trait Quant
+object Forall extends Quant
+object Exists extends Quant
+
+sealed abstract class Quantification(q: Quant, is: List[String], e: Expression) extends Expression {
+ val Q = q;
+ val Is = is;
+ val E = e;
+ var variables = null: List[Variable]; // resolved by type checker
+}
+case class SeqQuantification(q: Quant, is: List[String], seq: Expression, e: Expression) extends Quantification(q, is, e)
+case class TypeQuantification(q: Quant, is: List[String], t: Type, e: Expression) extends Quantification(q, is, e)
// sequences
@@ -387,7 +387,11 @@ case class Range(min: Expression, max: Expression /* non-inclusive*/) extends Ex
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)
+sealed abstract case class SeqAccess(e0: Expression, e1: Expression) extends BinaryExpr(e0, e1) {
+ override val ExpectedLhsType = null
+ override val ExpectedRhsType = null
+ override val ResultType = null
+}
case class Length(e: Expression) extends Expression
case class At(s: Expression, n: Expression) extends SeqAccess(s, n) {
override val OpName = ""
@@ -398,11 +402,10 @@ case class Drop(s: Expression, n: Expression) extends SeqAccess(s, n) {
case class Take(s: Expression, n: Expression) extends SeqAccess(s, n) {
override val OpName = ""
}
-case class Contains(s: Expression, n: Expression) extends SeqAccess(s, n) {
+case class Contains(n: Expression, s: Expression) extends SeqAccess(n, s) {
override val OpName = "in"
}
-
// eval
case class Eval(h: EvalState, e: Expression) extends Expression
@@ -419,3 +422,157 @@ case class CallState(token: Expression, obj: Expression, id: String, args: List[
var m = null: Method;
def target() = token;
}
+
+// visitors / operations
+
+object AST {
+ /**
+ * Transforms an expression using f. f must produce expressions of the appropriate type (e.g. not replace int literal with a bool literal)
+ * Ensures that mutable fields of expressions are carried over. f must make sure that mutable fields of its value are filled in.
+ */
+ def transform(expr: Expression, f: Expression => Option[Expression]):Expression = {
+ val func = (e:Expression) => transform(e, f);
+ val x = f(expr);
+ // apply recursively
+ val result = if (x isDefined) x.get else expr match {
+ case _:Literal => expr
+ case _:ThisExpr => expr
+ case _:Result => expr
+ case _:VariableExpr => expr
+ case ma@MemberAccess(e, id) =>
+ val g = MemberAccess(func(e), id);
+ g.f = ma.f;
+ g.predicate = ma.predicate;
+ g.isPredicate = ma.isPredicate;
+ g
+ case Full | Epsilon | Star => expr
+ case Frac(perm) => Frac(func(perm))
+ case Epsilons(perm) => Epsilons(func(perm))
+ case Access(e, perm) => Access(func(e).asInstanceOf[MemberAccess], func(perm).asInstanceOf[Permission]);
+ case AccessAll(obj, perm) => AccessAll(func(obj), func(perm).asInstanceOf[Permission]);
+ case AccessSeq(s, None, perm) => AccessSeq(func(s), None, func(perm).asInstanceOf[Permission])
+ case AccessSeq(s, Some(f), perm) => AccessSeq(func(s), Some(func(f).asInstanceOf[MemberAccess]), func(perm).asInstanceOf[Permission])
+ case Credit(e, None) => Credit(func(e), None)
+ case Credit(e, Some(n)) => Credit(func(e), Some(func(n)))
+ case Holds(e) => Holds(func(e))
+ case RdHolds(e) => RdHolds(func(e))
+ case _: Assigned => expr
+ 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[Access], 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 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 Contains(e0, e1) => Contains(func(e0), func(e1))
+ case qe @ SeqQuantification(q, is, seq, e) =>
+ val result = SeqQuantification(q, is, func(seq), func(e));
+ result.variables = qe.variables;
+ result;
+ case qe @ TypeQuantification(q, is, t, e) =>
+ val result = TypeQuantification(q, is, t, func(e));
+ result.variables = qe.variables;
+ result;
+ case Eval(h, e) =>
+ Eval(h match {
+ case AcquireState(obj) => AcquireState(func(obj))
+ case ReleaseState(obj) => ReleaseState(func(obj))
+ case cs @ CallState(token, obj, i, args) =>
+ val result = CallState(func(token), func(obj), i, args map { a => func(a)});
+ result.m = cs.m;
+ result;
+ }, func(e))
+ };
+
+ // preserve type
+ if (result.typ == null) result.typ = expr.typ;
+ // preserve position
+ if (result.pos == NoPosition) result.pos = expr.pos
+ result
+ }
+
+ // Applies recursively the function f first to the expression and then to its subexpressions (that is members of type RValue)
+ def visit(expr: RValue, f: RValue => Unit) {
+ f(expr);
+ expr match {
+ case _:Literal => ;
+ case _:ThisExpr => ;
+ case _:Result => ;
+ case _:VariableExpr => ;
+ case MemberAccess(e, _) =>
+ visit(e, f);
+
+ case Frac(p) => visit(p, f);
+ case Epsilons(p) => visit(p, f);
+ case Full | Epsilon | Star =>;
+ case Access(e, perm) =>
+ visit(e, f); visit(perm, f);
+ case AccessAll(obj, perm) =>
+ visit(obj, f); visit(perm, f);
+ case AccessSeq(s, _, perm) =>
+ visit(s, f); visit(perm, f);
+
+ case Credit(e, n) =>
+ visit(e, f); n match { case Some(n) => visit(n, f); case _ => }
+ case Holds(e) => visit(e, f);
+ case RdHolds(e) => visit(e, f);
+
+ case e: BinaryExpr =>
+ visit(e.E0, f); visit(e.E1, f);
+ case Range(min, max) =>
+ visit(min, f); visit(max, f);
+ case e: Assigned => e
+ case Old(e) => visit(e, f);
+ case IfThenElse(con, then, els) => visit(con, f); visit(then, f); visit(els, f);
+ case Not(e) => visit(e, f);
+ case funapp@FunctionApplication(obj, id, args) =>
+ visit(obj, f); args foreach { arg => visit(arg, f) };
+ case Unfolding(pred, e) =>
+ visit(pred, f); visit(e, f);
+
+ case SeqQuantification(_, _, seq, e) => visit(seq, f); visit(e, f);
+ case TypeQuantification(_, _, _, e) => visit(e, f);
+
+ case ExplicitSeq(es) =>
+ es foreach { e => visit(e, f) }
+ case Length(e) =>
+ visit(e, f)
+ case Eval(h, e) =>
+ h match {
+ case AcquireState(obj) => visit(obj, f);
+ case ReleaseState(obj) => visit(obj, f);
+ case CallState(token, obj, id, args) =>
+ visit(token, f); visit(obj, f); args foreach {a : Expression => visit(a, f)};
+ }
+ visit(e, f);
+ case NewRhs(_, init, lowerBounds, upperBounds) =>
+ lowerBounds foreach { e => visit(e, f)};
+ upperBounds foreach { e => visit(e, f)};
+ }
+ }
+} \ No newline at end of file
diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala
index 50404f2a..32593da5 100644
--- a/Chalice/src/Boogie.scala
+++ b/Chalice/src/Boogie.scala
@@ -68,8 +68,9 @@ object Boogie {
def apply(e: Expr, f: Expr) = new MapSelect(this, e, Some(f))
def apply(e: Expr) = new MapSelect(this, e, None)
def thenElse(thenE: Expr, elseE: Expr) = new Ite(this, thenE, elseE)
- def select(e: Expr, s: String) = new MapSelect(this, e, s)
+ def select(e: Expr, s: String) = new MapSelect(this, e, s) // useful for working on heap
def forall(x: BVar) = new Forall(x, this)
+ def exists(x: BVar) = new Exists(x, this)
def store(e: Expr, f: Expr, rhs: Expr) = MapUpdate(this, e, Some(f), rhs)
}
case class IntLiteral(n: Int) extends Expr
@@ -94,12 +95,13 @@ object Boogie {
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)
+ def this(x: BVar, body: Expr) = this(Nil, List(x), Nil, body)
+ def this(xs: List[BVar], triggers: List[Expr], body: Expr) = this(Nil, xs, triggers, body)
+ def this(t: TVar, x: BVar, body: Expr) = this(List(t), List(x), Nil, 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 Exists(ta: List[TVar], xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr {
+ def this(x: BVar, body: Expr) = this(Nil, List(x), List(), body)
+ def this(xs: List[BVar], triggers: List[Expr], body: Expr) = this(Nil, xs, triggers, body)
}
case class Lambda(ta: List[TVar], xs: List[BVar], body: Expr) extends Expr
@@ -274,8 +276,9 @@ object Boogie {
Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) +
PrintExpr(body) +
")"
- case Exists(xs, triggers, body) =>
+ case Exists(ts, xs, triggers, body) =>
"(exists " +
+ (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) + "} " }) +
diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala
index 0c35bd5b..0e9c5d39 100644
--- a/Chalice/src/ChaliceToCSharp.scala
+++ b/Chalice/src/ChaliceToCSharp.scala
@@ -56,7 +56,7 @@ class ChaliceToCSharp {
def convertMember(member: Member): String = {
member match {
- case Field(id, tp) =>
+ case Field(id, tp, false) =>
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) {
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 69c011a8..cfb41bc0 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -57,8 +57,8 @@ class Parser extends StandardTokenParsers {
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} }
+ ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id, t, false) }
+ | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id, t, true) }
)
def Ident =
positioned(ident ^^ PositionedString)
@@ -78,14 +78,15 @@ class Parser extends StandardTokenParsers {
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 methodDecl = {
+ currentLocalVariables = Set[String]()
+ "method" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~
+ (methodSpec*) ~ blockStatement ^^ {
+ case id ~ ins ~ outs ~ spec ~ body =>
+ outs match {
+ case None => Method(id, ins, Nil, spec, body)
+ case Some(outs) => Method(id, ins, outs, spec, body) }}
+ }
def channelDecl =
"channel" ~> ident ~ formalParameters(true) ~ ("where" ~> expression ?) <~ Semi ^^ {
case id ~ ins ~ None => Channel(id, ins, BoolLiteral(true))
@@ -476,21 +477,37 @@ class Parser extends StandardTokenParsers {
| ("ite" ~> "(" ~> expression <~ ",") ~ (expression <~ ",") ~ (expression <~ ")") ^^ {
case con ~ then ~ els => IfThenElse (con, then, els) }
| "(" ~> expression <~ ")"
- | forall
+ | quantifierType
+ | quantifierSeq
| ("[" ~> expression) ~ (":" ~> expression <~ "]") ^^ { case from ~ to => Range(from, to) }
| ("nil" ~> "<") ~> (typeDecl <~ ">") ^^ EmptySeq
| ("[" ~> expressionList <~ "]") ^^ { case es => ExplicitSeq(es) }
)
- def forall: Parser[Quantification] =
- (("forall" | "exists") ~ repsep(ident, ",") <~ "in") into {case quant ~ is => quantifierBody(quant, is)}
- def quantifierBody(quant: String, is: List[String]) : Parser[Quantification] =
- ((expression <~ "::") ~ (exprWithLocals(is))) ^^
+ // Scala type inference resists figuring out | (alternative) for these two
+
+ def quantifierSeq: Parser[Quantification] =
+ (quant ~ repsep(ident, ",")) into {case q ~ is => quantifierSeqBody(q, is)}
+
+ def quantifierSeqBody(q: Quant, is: List[String]) : Parser[Quantification] =
+ (("in" ~> expression <~ "::") ~ (exprWithLocals(is))) ^^
{ case seq ~ e =>
- val result = quant match {case "forall" => Forall(is, seq, e); case "exists" => Exists(is, seq, e);};
currentLocalVariables = currentLocalVariables -- is;
- result
- }
+ SeqQuantification(q, is, seq, e);
+ }
+
+ def quantifierType: Parser[Quantification] =
+ (quant ~ repsep(ident, ",")) into {case q ~ is => quantifierTypeBody(q, is)}
+
+ def quantifierTypeBody(q: Quant, is: List[String]) : Parser[Quantification] =
+ ((":" ~> typeDecl <~ "::") ~ (exprWithLocals(is))) ^^
+ { case t ~ e =>
+ currentLocalVariables = currentLocalVariables -- is;
+ TypeQuantification(q, is, t, e);
+ }
+
+ def quant: Parser[Quant] =
+ ( "forall" ^^^ Forall | "exists" ^^^ Exists)
def exprWithLocals(i: List[String]) : Parser[Expression] = {
currentLocalVariables = currentLocalVariables ++ i;
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index 82e7658c..205349c6 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -18,8 +18,8 @@ object PrintProgram {
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.FullName + Semi)
+ case f@ Field(id, t, ghost) =>
+ println(" " + (if (ghost) "ghost " else "") + "var " + id + ": " + t.FullName + Semi)
case m: Method =>
print(" method " + m.id)
print("("); VarList(m.ins); print(")")
@@ -257,12 +257,16 @@ object PrintProgram {
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 + " ");
+ print("(" + (q.Q match {case Forall => "forall"; case Exists => "exists"}) + " ");
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(")");
+ q match {
+ case q: SeqQuantification => print(" in "); Expr(q.seq);
+ case q: TypeQuantification => print(": "); print(q.t.typ.FullName);
+ }
+ print(" :: "); Expr(q.E); print(")");
case EmptySeq(t) =>
print("nil<"); print(t.FullName); print(">");
case ExplicitSeq(es) =>
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index c14b68c8..6ea3e155 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -78,9 +78,9 @@ object Resolver {
case cl: Class =>
for (m <- cl.asInstanceOf[Class].members) m match {
case _:MonitorInvariant =>
- case Field(id,t) =>
+ case Field(_, t, _) =>
ResolveType(t, contextNoCurrentClass)
- case Method(id, ins, outs, spec, body) =>
+ case Method(_, ins, outs, _, _) =>
for (v <- ins ++ outs) {
ResolveType(v.t, contextNoCurrentClass)
}
@@ -101,7 +101,7 @@ object Resolver {
// * VariableExpr and FieldSelect expressions
for (decl <- prog) decl match {
case ch: Channel =>
- val context = new ProgramContext(decls, ChannelClass(ch))
+ val context = new ProgramContext(decls, ChannelClass(ch))
var ctx = context
for (v <- ch.parameters) {
ctx = ctx.AddVariable(v)
@@ -276,11 +276,11 @@ object Resolver {
}
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 != 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)
+ 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(declaresLocal, lhs, obj, id, args) =>
ResolveExpr(obj, context, false, false)(false)
@@ -361,11 +361,11 @@ object Resolver {
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.")
+ if(!e.ma.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.")
+ if(!e.ma.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)
@@ -575,7 +575,7 @@ object Resolver {
} else {
fieldNames = fieldNames + f
e.typ.LookupMember(f) match {
- case Some(field@Field(name, tp)) =>
+ 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 + ".");
@@ -715,7 +715,7 @@ object Resolver {
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.")
+ if(! pred.ma.isPredicate) context.Error(uf.pos, "Only predicates can be unfolded.")
uf.typ = e.typ;
case bin: EqualityCompareExpr =>
ResolveExpr(bin.E0, context, twoStateContext, false)
@@ -777,16 +777,26 @@ object Resolver {
" (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);
+ q.Is foreach { i => if(context.LookupVariable(i).isDefined) context.Error(q.pos, "The variable " + i + " hides another local.") };
+ val typ = q match {
+ case q: SeqQuantification =>
+ 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 + ").");
+ None;
+ } else
+ Some(q.seq.typ.parameters(0));
+ case q: TypeQuantification =>
+ ResolveType(q.t, context);
+ if (q.t.typ == null) None else Some(q.t.typ);
+ };
+
+ if (typ.isDefined) {
+ val vartype = typ.get;
var bodyContext = context;
var bvariables = Nil: List[Variable];
q.Is foreach { i =>
- val variable = new Variable(i, new Type(elementType));
+ val variable = new Variable(i, new Type(vartype));
bodyContext = bodyContext.AddVariable(variable);
bvariables = bvariables ::: List(variable);
}
@@ -895,27 +905,26 @@ object Resolver {
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)
+ if (!fs.isPredicate && fs.f != null && fs.f.isGhost) context.Error(fs.pos, "ghost fields not allowed here")
case a: Assigned =>
if (a.v != null && a.v.IsGhost) context.Error(a.pos, "ghost variable not allowed here")
- case _ => visitE(e, specOk)
+ case _ => // do nothing
}
}
- specOk(expr)
+ AST.visit(expr, specOk);
}
def CheckNoImmutableGhosts(expr: RValue, context: ProgramContext): Unit = {
- def specOk(e: RValue): 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)
+ case _ => // do nothing
}
}
- specOk(expr)
+ AST.visit(expr, specOk);
}
def CheckRunSpecification(e: Expression, context: ProgramContext, allowMaxLock: Boolean): Unit = e match {
@@ -972,8 +981,10 @@ object Resolver {
case bin: BinaryExpr =>
CheckRunSpecification(bin.E0, context, false)
CheckRunSpecification(bin.E1, context, false)
- case q: Quantification =>
- CheckRunSpecification(q.Seq, context, false)
+ case q: SeqQuantification =>
+ CheckRunSpecification(q.seq, context, false)
+ CheckRunSpecification(q.E, context, true)
+ case q: TypeQuantification =>
CheckRunSpecification(q.E, context, true)
case Length(e) =>
CheckRunSpecification(e, context, false);
@@ -990,77 +1001,4 @@ object Resolver {
}
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 Frac(p) => func(p);
- case Epsilons(p) => func(p);
- case Full | Epsilon | Star =>;
- case Access(e, perm) =>
- func(e); visitE(perm, func);
- case AccessAll(obj, perm) =>
- func(obj); visitE(perm, func);
- case AccessSeq(s, f, perm) =>
- func(s); visitE(perm, func);
- case Credit(e, n) =>
- func(e); n match { case Some(n) => func(n); 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 Exists(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 Contains(s, n) => func(s); func(n);
- 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
index ff840986..2bfbd69f 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -4,6 +4,7 @@
//
//-----------------------------------------------------------------------------
import scala.util.parsing.input.Position
+import scala.util.parsing.input.NoPosition
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,
@@ -579,7 +580,7 @@ class Translator {
} :::
// exhale preconditions
Exhale(Preconditions(c.m.spec) map
- (p => SubstVars(p, Some(formalThis), c.m.ins, formalIns)) zip (Preconditions(c.m.spec) map { p => ErrorMessage(c.pos, "The precondition at " + p.pos + " might not hold.")}), "precondition") :::
+ (p => SubstVars(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
@@ -637,7 +638,7 @@ class Translator {
etran.SetNoPermission(token, "joinable", etran.Mask) ::
// inhale postcondition of the call
postEtran.Inhale(Postconditions(jn.m.spec) map
- { p => SubstVars(p, Some(formalThis), jn.m.ins ++ jn.m.outs, formalIns ++ formalOuts)}, "postcondition", false) :::
+ { p => SubstVars(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))
case s@Send(ch, args) =>
@@ -660,7 +661,7 @@ class Translator {
new Boogie.MapUpdate(etran.Credits, TrExpr(ch), new Boogie.MapSelect(etran.Credits, TrExpr(ch)) + 1) ::
// exhale where clause
Exhale(List(
- (SubstVars(channel.where, Some(formalThis), channel.parameters, formalParams),
+ (SubstVars(channel.where, formalThis, channel.parameters, formalParams),
ErrorMessage(s.pos, "The where clause at " + channel.where.pos + " might not hold."))),
"channel where clause")
case r@Receive(_, ch, outs) =>
@@ -684,7 +685,7 @@ class Translator {
(formalThis := ch) ::
(for (v <- formalParams) yield Havoc(v)) :::
// inhale where clause
- Inhale(List(SubstVars(channel.where, Some(formalThis), channel.parameters, formalParams)), "channel where clause") :::
+ Inhale(List(SubstVars(channel.where, formalThis, channel.parameters, formalParams)), "channel where clause") :::
// declare any new local variables among the actual outs
(for (v <- r.locals) yield BLocal(Variable2BVarWhere(v))) :::
// assign formal outs to actual outs
@@ -820,14 +821,14 @@ class Translator {
(for ((v,e) <- formalIns zip args) yield (v := e)) :::
// exhale preconditions
Exhale(Preconditions(c.m.spec) map
- (p => SubstVars(p, Some(formalThis), c.m.ins, formalIns)) zip (Preconditions(c.m.spec) map { p => ErrorMessage(c.pos, "The precondition at " + p.pos + " might not hold.")}), "precondition") :::
+ (p => SubstVars(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 => SubstVars(p, Some(formalThis), c.m.ins, formalIns))) yield etran.Tr(e), postEtran) :::
+ LockHavoc(for (e <- LockChanges(c.m.spec) map (p => SubstVars(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 => SubstVars(p, Some(formalThis), c.m.ins ++ c.m.outs, formalIns ++ formalOuts)) , "postcondition", false) :::
+ (p => SubstVars(p, formalThis, c.m.ins ++ c.m.outs, formalIns ++ formalOuts)) , "postcondition", false) :::
// declare any new local variables among the actual outs
(for (v <- c.locals) yield BLocal(Variable2BVarWhere(v))) :::
// assign formal outs to actual outs
@@ -846,9 +847,9 @@ class Translator {
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, None, w.LoopTargetsList,
+ val lkchOld = lkch map (e => SubstVars(e, w.LoopTargetsList,
for (v <- saveLocalsV) yield new VariableExpr(v)))
- val lkchIterStart = lkch map (e => SubstVars(e, None, w.LoopTargetsList,
+ 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))
@@ -1147,10 +1148,10 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
**********************************************************************/
def isDefined(e: Expression)(implicit assumption: Expr): List[Boogie.Stmt] = {
- def prove(goal: Expr, pos: Position, msg: String)(implicit assumption: Expr): Boogie.Assert = {
+ def prove(goal: Expr, pos: Position, msg: String)(implicit assumption: Expr) =
bassert(assumption ==> goal, pos, msg)
- }
- e match {
+
+ desugar(e) match {
case IntLiteral(n) => Nil
case BoolLiteral(b) => Nil
case NullLiteral() => Nil
@@ -1198,7 +1199,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
BLocal(tmpHeapV) :: (tmpHeap := Heap) ::
BLocal(tmpMaskV) :: (tmpMask := Mask) :::
BLocal(tmpCreditsV) :: (tmpCredits := Credits) :::
- tmpTranslator.Exhale(Preconditions(func.f.spec) map { pre=> (SubstVars(pre, Some(obj), func.f.ins, args), ErrorMessage(func.pos, "Precondition at " + pre.pos + " might not hold."))},
+ tmpTranslator.Exhale(Preconditions(func.f.spec) map { pre=> (SubstVars(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
@@ -1260,16 +1261,6 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
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) =>
- isDefinedQuantification(q.variables, min, max, e)
- case q@Exists(i, Range(min, max), e) =>
- isDefinedQuantification(q.variables, min, max, e)
- case q@Forall(i, seq, e) =>
- var newVars = q.variables map (v => new Variable(v.UniqueName, new Type(IntClass)))
- isDefinedQuantification(newVars, IntLiteral(0), Length(seq), SubstVars(e, None, q.variables, newVars map {v => At(seq, new VariableExpr(v)) }))
- case q@Exists(i, seq, e) =>
- var newVars = q.variables map (v => new Variable(v.UniqueName, new Type(IntClass)))
- isDefinedQuantification(newVars, IntLiteral(0), Length(seq), SubstVars(e, None, q.variables, newVars map {v => At(seq, new VariableExpr(v)) }))
case EmptySeq(t) => Nil
case ExplicitSeq(es) =>
es flatMap { e => isDefined(e) }
@@ -1280,15 +1271,15 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
case at@At(e0, e1) =>
isDefined(e0) ::: isDefined(e1) :::
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.")
+ prove(Tr(e1) < SeqLength(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) :::
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.")
+ prove(Tr(e1) <= SeqLength(Tr(e0)), e.pos, "Cannot drop more than elements than the length of the sequence.")
case Take(e0, e1) =>
isDefined(e0) ::: isDefined(e1) :::
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.")
+ prove(Tr(e1) <= SeqLength(Tr(e0)), e.pos, "Cannot take more than elements than the length of the sequence.")
case Length(e) =>
isDefined(e)
case Contains(e0, e1) =>
@@ -1297,28 +1288,16 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
val (evalHeap, evalMask, evalCredits, checks, assumptions) = fromEvalState(h);
val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);
evalEtran.isDefined(e)
+ case _ : SeqQuantification => throw new Exception("should be desugared")
+ case tq @ TypeQuantification(_, _, _, e) =>
+ // replace variables since we need locals
+ val vars = tq.variables map {v => val result = new Variable(v.id, v.t); result.pos = v.pos; result;}
+ (vars map {v => BLocal(Boogie.BVar(v.UniqueName, type2BType(v.t.typ)))}) :::
+ isDefined(SubstVars(e, tq.variables, vars map {v => new VariableExpr(v);}))
}
}
- def isDefinedQuantification(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 = iTmp :: iTmps;
- 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, tint))
- }) :::
- // prove that the body is well-defined for iTmp, provided iTmp lies between min and max
- isDefined(SubstVars(e, None, is, iTmps map { iTmp => new VariableExpr(iTmp)}))(assumption2)
- }
-
- def Tr(e: Expression): Boogie.Expr = e match {
+ def Tr(e: Expression): Boogie.Expr = desugar(e) match {
case IntLiteral(n) => n
case BoolLiteral(b) => b
case NullLiteral() => bnull
@@ -1409,8 +1388,6 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
Tr(e0) / Tr(e1)
case Mod(e0,e1) =>
Tr(e0) % Tr(e1)
- case q: Quantification =>
- translateQuantification(q)
case EmptySeq(t) =>
createEmptySeq
case ExplicitSeq(es) =>
@@ -1423,44 +1400,22 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
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 at@At(e0, e1) =>SeqIndex(Tr(e0), Tr(e1))
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 Contains(e0, e1) =>
- Boogie.FunctionApp("Seq#Contains", List(Tr(e1), Tr(e0)))
+ case Length(e) => SeqLength(e)
+ case Contains(e0, e1) => SeqContains(Tr(e1), Tr(e0))
case Eval(h, e) =>
val (evalHeap, evalMask, evalCredits, checks, assumptions) = fromEvalState(h);
val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);
evalEtran.Tr(e)
- }
-
- def translateQuantification(q: Quantification): Expr = {
- // generate index variables
- var (is, min, max, e) = q match {
- case Forall(_, Range(min, max), e) => (q.variables, min, max, e);
- case Exists(_, Range(min, max), e) => (q.variables, min, max, e);
- case Forall(_, seq, eo) =>
- var is = q.variables map (v => new Variable(v.UniqueName, new Type(IntClass)));
- var e = SubstVars(eo, None, q.variables, is map {v => At(seq, new VariableExpr(v))});
- (is, IntLiteral(0), Length(seq), e);
- case Exists(_, seq, eo) =>
- var is = q.variables map (v => new Variable(v.UniqueName, new Type(IntClass)));
- var e = SubstVars(eo, None, q.variables, is map {v => At(seq, new VariableExpr(v))});
- (is, IntLiteral(0), Length(seq), e);
- }
- var assumption = true: Expr;
- for(i <- is) {
- assumption = assumption && (Tr(min) <= VarExpr(i.UniqueName) && VarExpr(i.UniqueName) < Tr(max));
- }
- q match {
- case _: Forall => new Boogie.Forall(is map { i => Variable2BVar(i)}, Nil, assumption ==> Tr(e));
- case _: Exists => new Boogie.Exists(is map { i => Variable2BVar(i)}, Nil, assumption && Tr(e));
- }
+ case _:SeqQuantification => throw new Exception("should be desugared")
+ case tq @ TypeQuantification(Forall, _, _, e) =>
+ new Boogie.Forall(tq.variables map { v => Variable2BVar(v)}, Nil, Tr(e))
+ case tq @ TypeQuantification(Exists, _, _, e) =>
+ new Boogie.Exists(tq.variables map { v => Variable2BVar(v)}, Nil, Tr(e))
}
def ShaveOffOld(e: Expression): (Expression, Boolean) = e match {
@@ -1500,24 +1455,13 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
Comment("end inhale")
}
- def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean): List[Boogie.Stmt] = p match {
+ def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean): List[Boogie.Stmt] = desugar(p) match {
case pred@MemberAccess(e, p) if pred.isPredicate =>
val tmp = Access(pred, Full);
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 AccessSeq(s, None, perm) =>
- s.typ.parameters(0).Fields flatMap { f =>
- val ma = MemberAccess(At(s, IntLiteral(0)), f.id); ma.f = f; ma.pos = p.pos;
- val inhalee = AccessSeq(s, Some(ma), perm); inhalee.pos = p.pos;
- Inhale(inhalee, ih, check) }
+ case AccessAll(obj, perm) => throw new Exception("should be desugared")
+ case AccessSeq(s, None, perm) => throw new Exception("should be desugared")
case acc@Access(e,perm) =>
val trE = Tr(e.e)
val module = currentClass.module;
@@ -1559,9 +1503,9 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
val (refV, ref) = Boogie.NewBVar("ref", tref, true);
val (fV, f) = Boogie.NewBVar("f", FieldType(a), true);
(Heap := Lambda(List(aV), List(refV, fV),
- (FunctionApp("Seq#Contains", List(e, ref)) && f ==@ memberName).thenElse
+ (SeqContains(e, ref) && f ==@ memberName).thenElse
(ih(ref, f), Heap(ref, f)))) ::
- bassume((FunctionApp("Seq#Contains", List(e, ref)) ==> TypeInformation(Heap(ref, memberName), member.f.typ.typ)).forall(refV))
+ bassume((SeqContains(e, ref) ==> TypeInformation(Heap(ref, memberName), member.f.typ.typ)).forall(refV))
} :::
bassume(wf(Heap, Mask)) ::
{
@@ -1570,7 +1514,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
val (fV, f) = Boogie.NewBVar("f", FieldType(a), true);
val (pcV,pc) = Boogie.NewBVar("p", tperm, true);
Mask := Lambda(List(aV), List(refV, fV),
- (FunctionApp("Seq#Contains", List(e, ref)) && f ==@ memberName).thenElse
+ (SeqContains(e, ref) && f ==@ memberName).thenElse
(Lambda(List(), List(pcV),
Boogie.Ite(pc ==@ "perm$R",
Mask(ref, f)("perm$R") + r,
@@ -1649,24 +1593,13 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
Comment("end exhale")
}
- def Exhale(p: Expression, em: Boogie.Expr, eh: Boogie.Expr, error: ErrorMessage, check: Boolean): List[Boogie.Stmt] = p match {
+ def Exhale(p: Expression, em: Boogie.Expr, eh: Boogie.Expr, error: ErrorMessage, check: Boolean): List[Boogie.Stmt] = desugar(p) match {
case pred@MemberAccess(e, p) if pred.isPredicate =>
val tmp = Access(pred, Full);
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 AccessSeq(s, None, perm) =>
- s.typ.parameters(0).Fields flatMap { f =>
- val ma = MemberAccess(At(s, IntLiteral(0)), f.id); ma.f = f; ma.pos = p.pos;
- val exhalee = AccessSeq(s, Some(ma), perm); exhalee.pos = p.pos;
- Exhale(exhalee, em, eh, error, check) }
+ case AccessAll(obj, perm) => throw new Exception("should be desugared")
+ case AccessSeq(s, None, perm) => throw new Exception("should be desugared")
case acc@Access(e,perm:Write) =>
val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
@@ -1751,13 +1684,13 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
val mr = em(ref, memberName)("perm$R");
val mn = em(ref, memberName)("perm$N");
- bassert((FunctionApp("Seq#Contains", List(e, ref)) ==>
+ bassert((SeqContains(e, ref) ==>
(perm match {
case _: Read => mr ==@ 0 ==> n <= mn
case _: Write => r <= mr && (r ==@ mr ==> 0 <= mn)
})).forall(refV), error.pos, error.message + " Insufficient permissions") ::
(em := Lambda(List(aV), List(refV, fV),
- (FunctionApp("Seq#Contains", List(e, ref)) && f ==@ memberName).thenElse(
+ (SeqContains(e, ref) && f ==@ memberName).thenElse(
Lambda(List(), List(pcV), (pc ==@ "perm$R").thenElse(mr - r, mn - n)),
em(ref, f))))
} :::
@@ -1835,6 +1768,79 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
}
}
+
+ // De-sugar expression (idempotent)
+ // * unroll wildcard pattern (for objects) in permission expression
+ // * convert sequence quantification into type quantification
+ def desugar(expr: Expression): Expression = expr transform {
+ _ match {
+ case AccessAll(obj, perm) =>
+ Some(obj.typ.Fields.map({f =>
+ val ma = MemberAccess(desugar(obj), f.id);
+ ma.f = f; ma.pos = expr.pos; ma.typ = f.typ.typ;
+ val acc = Access(ma, perm);
+ acc.pos = expr.pos; acc.typ = acc.typ; acc
+ }).foldLeft(BoolLiteral(true): Expression){(e1, e2) =>
+ val and = And(e1, e2);
+ and.pos = expr.pos; and.typ = BoolClass; and
+ })
+ case AccessSeq(s, None, perm) =>
+ Some(s.typ.parameters(0).Fields.map({(f) =>
+ val ma = MemberAccess(At(desugar(s), IntLiteral(0)), f.id);
+ ma.f = f; ma.pos = expr.pos; ma.typ = f.typ.typ;
+ val acc = AccessSeq(s, Some(ma), perm);
+ acc.pos = expr.pos; acc.typ = acc.typ; acc
+ }).foldLeft(BoolLiteral(true): Expression){(e1, e2) =>
+ val and = And(e1, e2);
+ and.pos = expr.pos; and.typ = BoolClass; and
+ })
+ case qe @ SeqQuantification(q, is, Range(min, max), e) =>
+ val dmin = desugar(min);
+ val dmax = desugar(max);
+ val dis = qe.variables;
+ val disx = dis map {v => new VariableExpr(v)};
+ val de = desugar(e);
+
+ val assumption = disx map {x =>
+ And(AtMost(dmin, x), Less(x, dmax))
+ } reduceLeft {(e0, e1) =>
+ And(e0, e1)
+ };
+ assumption transform {e => e.pos = expr.pos; None};
+ val body = q match {
+ case Forall => Implies(assumption, de);
+ case Exists => And(assumption, de);
+ }
+ body.pos = expr.pos;
+ val result = TypeQuantification(q, is, new Type(IntClass), body);
+ result.variables = dis;
+ Some(result);
+ case qe @ SeqQuantification(q, is, seq, e) =>
+ val dseq = desugar(seq);
+ val min = IntLiteral(0);
+ val max = Length(dseq);
+ val dis = qe.variables map {v => new Variable(v.UniqueName, new Type(IntClass))};
+ val disx = dis map {v => new VariableExpr(v)};
+ val de = SubstVars(desugar(e), qe.variables, disx map {x => At(dseq, x)});
+
+ val assumption = disx map {x =>
+ And(AtMost(min, x), Less(x, max))
+ } reduceLeft {(e0, e1) =>
+ And(e0, e1)
+ };
+ assumption transform {e => e.pos = expr.pos; None};
+ val body = q match {
+ case Forall => Implies(assumption, de);
+ case Exists => And(assumption, de);
+ }
+ body.pos = expr.pos;
+ val result = TypeQuantification(q, is, new Type(IntClass), body);
+ result.variables = dis;
+ Some(result);
+ case _ => None;
+ }
+ }
+
// permissions
def CanRead(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = new Boogie.FunctionApp("CanRead", Mask, obj, field)
@@ -2077,11 +2083,17 @@ object TranslationHelper {
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 cast(a: Expr, b: Expr) = FunctionApp("cast", List(a, b))
+
+ // Sequences
+
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))
+ def SeqLength(s: Expr) = FunctionApp("Seq#Length", List(s))
+ def SeqContains(s: Expr, elt: Expr) = FunctionApp("Seq#Contains", List(s, elt))
+ def SeqIndex(s: Expr, idx: Expr) = FunctionApp("Seq#Index", List(s, idx))
def Variable2BVar(v: Variable) = new Boogie.BVar(v.UniqueName, v.t.typ)
def Variable2BVarWhere(v: Variable) = NewBVarWhere(v.UniqueName, v.t)
@@ -2137,16 +2149,14 @@ object TranslationHelper {
(e ==@ Boogie.Null()) || (dtype(e) ==@ className(cl))
} else if (cl.IsSeq && cl.parameters(0).IsRef) {
val (v,ve) = Boogie.NewBVar("$i", tint, true);
- new Boogie.Forall(List(v), Nil,
- 0 <= ve && ve < Boogie.FunctionApp("Seq#Length", List(e)) ==>
- TypeInformation(Boogie.FunctionApp("Seq#Index", List(e,ve)), cl.parameters(0)));
+ (0 <= ve && ve < SeqLength(e)
+ ==> TypeInformation(SeqIndex(e,ve), cl.parameters(0))).forall(v);
} else {
true
}
}
- def Version(expr: Expression, etran: ExpressionTranslator): Boogie.Expr =
- {
+ def Version(expr: Expression, etran: ExpressionTranslator): Boogie.Expr = {
expr match{
case pred@MemberAccess(e, p) if pred.isPredicate =>
Version(Access(pred, Full), etran)
@@ -2162,26 +2172,7 @@ object TranslationHelper {
case e => Boogie.VarExpr("nostate")
}
}
- /* Unused code that would fail for a nontrivial class
- 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)
@@ -2258,10 +2249,6 @@ object TranslationHelper {
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) =>
@@ -2301,160 +2288,63 @@ object TranslationHelper {
def SubstRd(e: Expression): Expression = e match {
case Access(e, _:Write) =>
- val r = Access(e,Epsilon); r.typ = BoolClass; r
- case Access(_, _:Read) => e
+ val r = Access(e,Epsilon); r.pos = e.pos; r.typ = BoolClass; r
case Implies(e0,e1) =>
- val r = Implies(e0, SubstRd(e1)); r.typ = BoolClass; r
+ val r = Implies(e0, SubstRd(e1)); r.pos = e.pos; r.typ = BoolClass; r
case And(e0,e1) =>
- val r = And(SubstRd(e0), SubstRd(e1)); r.typ = BoolClass; r
- case e => e
+ val r = And(SubstRd(e0), SubstRd(e1)); r.pos = e.pos; r.typ = BoolClass; r
+ case _ => e
}
def UnfoldPredicatesWithReceiverThis(expr: Expression): Expression = {
- def unfoldPred(e: Expression): Expression = {
+ val func = (e:Expression) =>
e match {
case pred@MemberAccess(o, f) if pred.isPredicate && o.isInstanceOf[ThisExpr] =>
- SubstThis(DefinitionOf(pred.predicate), o)
+ Some(SubstThis(DefinitionOf(pred.predicate), o))
case Access(pred@MemberAccess(o, f), p) if pred.isPredicate && o.isInstanceOf[ThisExpr] =>
- p match {
+ Some(p match {
case Full => SubstThis(DefinitionOf(pred.predicate), o)
case Frac(p) => FractionOf(SubstThis(DefinitionOf(pred.predicate), o), p)
case Epsilon => EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), o), IntLiteral(1))
case Star => throw new Exception("not supported yet")
case Epsilons(p) => EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), o), p)
- }
+ })
case func@FunctionApplication(obj: ThisExpr, name, args) if 2<=TranslationOptions.defaults =>
- SubstVars(func.f.definition, Some(obj), func.f.ins, args)
- case _ => manipulate(e, {ex => unfoldPred(ex)})
+ Some(SubstVars(func.f.definition, obj, func.f.ins, args))
+ case _ => None
}
- }
- unfoldPred(expr)
+ AST.transform(expr, func)
}
// needed to do a _simultaneous_ substitution!
- def SubstVars(expr: Expression, thisReplacement: Option[Expression], vs: List[Variable], xs: List[Expression]): Expression = {
- def replace(e: Expression, sub: List[(Variable, Expression)]): Expression = {
- e match {
- case _: ThisExpr =>
- thisReplacement match {
- case Some(e) => e;
- case None => e;
- }
- case e: VariableExpr =>
- // TODO: this will update the value of x's position many times -- better than none
- for ((v,x) <- sub if v == e.v) { x.pos = v.pos; x.typ = e.typ; return x }
- e
- case q: Quantification =>
- // would be better if this is a part of manipulate method
- val newSub = sub filter { xv => q.Is forall { variable => ! variable.id.equals(xv._1)}};
- val result = q match {
- case _ : Forall => Forall(q.Is, replace(q.Seq, sub), replace(q.E, newSub));
- case _ : Exists => Exists(q.Is, replace(q.Seq, sub), replace(q.E, newSub));
- }
- result.variables = q.variables;
- result.typ = q.typ;
- result.pos = q.pos;
- result
- case _ => manipulate(e, {ex => replace(ex, sub)})
- }
- }
- replace(expr, vs zip xs)
- }
-
- def SubstThis(expr: Expression, x: Expression): Expression = {
- def replaceThis(e: Expression): Expression = {
- e match {
- case _: ThisExpr => x
- case _ => manipulate(e, {ex => replaceThis(ex)})
- }
+ def SubstVars(expr: Expression, x:Expression, vs:List[Variable], es:List[Expression]): Expression =
+ SubstVars(expr, Some(x), Map() ++ (vs zip es));
+ def SubstVars(expr: Expression, vs:List[Variable], es:List[Expression]): Expression =
+ SubstVars(expr, None, Map() ++ (vs zip es));
+ def SubstVars(expr: Expression, t: Option[Expression], vs: Map[Variable, Expression]): Expression = expr.transform {
+ _ match {
+ case _: ThisExpr if t.isDefined => t
+ case e: VariableExpr =>
+ if (vs.contains(e.v)) Some(vs(e.v)) else None;
+ case q: Quantification =>
+ q.variables foreach { (v) => if (vs.contains(v)) throw new Exception("cannot substitute a variable bound in the quantifier")}
+ None;
+ case _ => None;
}
- 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)})
- }
+ def SubstThis(expr: Expression, x: Expression): Expression = expr.transform {
+ _ match {
+ case _: ThisExpr => Some(x)
+ case _ => None
}
- replaceThis(expr)
}
- /** Applies function to the children of an AST node but not the node itself. */
- 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 Full | Epsilon | Star => expr
- case Frac(perm) => Frac(func(perm))
- case Epsilons(perm) => Epsilons(func(perm))
- case Access(e, perm) => Access(func(e).asInstanceOf[MemberAccess], manipulate(perm, func).asInstanceOf[Permission]);
- case AccessAll(obj, perm) => AccessAll(func(obj), manipulate(perm, func).asInstanceOf[Permission]);
- case AccessSeq(s, None, perm) => AccessSeq(func(s), None, manipulate(perm, func).asInstanceOf[Permission])
- case AccessSeq(s, Some(f), perm) => AccessSeq(func(s), Some(func(f).asInstanceOf[MemberAccess]), manipulate(perm, func).asInstanceOf[Permission])
- case Credit(e, None) => Credit(func(e), None)
- case Credit(e, Some(n)) => Credit(func(e), Some(func(n)))
- case Holds(e) => Holds(func(e))
- 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[Access], 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 exists@Exists(i, seq, e) => val result = Exists(i, func(seq), func(e)); result.variables = exists.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 Contains(e0, e1) =>
- Contains(func(e0), func(e1))
- 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;
+ def SubstResult(expr: Expression, x: Expression): Expression = expr.transform {
+ _ match {
+ case _: Result => Some(x)
+ case _ => None
}
- result.pos = expr.pos
- result
}
}
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-18 14:43:32 +0000