From 21f3ed8dbd82da63302feafc72f3504499998569 Mon Sep 17 00:00:00 2001 From: kyessenov Date: Tue, 20 Jul 2010 01:01:28 +0000 Subject: Chalice: extended substitutor to handle "exists" quantifier and sequence containment; refactoring and preparing to extend wild card permissions to sequences --- Chalice/src/Parser.scala | 24 +++++----- Chalice/src/Translator.scala | 105 +++++++++++++++++++++---------------------- 2 files changed, 65 insertions(+), 64 deletions(-) (limited to 'Chalice') diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index 097526b0..123ead89 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -350,7 +350,7 @@ class Parser extends StandardTokenParsers { }) def CompareOp = "==" | "!=" | "<" | "<=" | ">=" | ">" | "<<" | "in" | "!in" def concatExpr = - positioned(addExpr ~ ("++" ~> addExpr *) ^^ { + positioned(addExpr ~ ("++" ~> addExpr *) ^^ { case e0 ~ rest => (rest foldLeft e0) { case (a, b) => Append(a, b) }}) def addExpr = @@ -436,20 +436,24 @@ class Parser extends StandardTokenParsers { val r = FunctionApplication(implicitThis, id.v, args) r.pos = id.pos; r } - | "rd" ~> - ( "holds" ~> "(" ~> expression <~ ")" ^^ RdHolds - | "(" ~> - ( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result})) ~ rdPermArg <~ ")" - | selectExprFerSureX ~ rdPermArg <~ ")" - ) ^^ { case MemberAccess(obj, "*") ~ p => RdAccessAll(obj, p) case e ~ p => RdAccess(e,p) } - ) + | "rd" ~> "(" ~> + ( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result})) ~ rdPermArg <~ ")" + | selectExprFerSureX ~ 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 ?) <~ ")" - | selectExprFerSureX ~ ("," ~> expression ?) <~ ")" - ) ^^ { case MemberAccess(obj, "*") ~ perm => AccessAll(obj, perm) case e ~ perm => Access(e, perm) } + | selectExprFerSureX ~ ("," ~> expression ?) <~ ")" + ) ^^ { + case MemberAccess(obj, "*") ~ perm => AccessAll(obj, perm); + case e ~ perm => Access(e, perm) + } | "credit" ~> "(" ~> expression ~ ("," ~> expression ?) <~ ")" ^^ { case ch ~ n => Credit(ch, n) } | "holds" ~> "(" ~> expression <~ ")" ^^ Holds + | "rd" ~> "holds" ~> "(" ~> expression <~ ")" ^^ RdHolds | "assigned" ~> "(" ~> ident <~ ")" ^^ Assigned | "old" ~> "(" ~> expression <~ ")" ^^ Old | ("unfolding" ~> suffixExpr <~ "in") ~ expression ^? { diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 1983b034..c4934a43 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -15,7 +15,7 @@ case class ErrorMessage(pos: Position, message: String) object TranslationOptions { // note: the initial values should match those Chalice.scala - var defaults = 0: int; + var defaults = 0: Int; var autoFold = false: Boolean; var checkLeaks = false: Boolean; var autoMagic = false: Boolean; @@ -41,14 +41,14 @@ class Translator { def translateClass(cl: Class): List[Decl] = { currentClass = cl; etran = new ExpressionTranslator(cl); - var declarations = Nil: List[Decl] + var declarations: List[Decl] = Nil; // 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; + declarations = Const(ModuleName(cl), true, ModuleType) :: declarations; + modules = cl.module :: modules; } // add class name - declarations = declarations + Const(cl.id + "#t", true, TypeName); + declarations = Const(cl.id + "#t", true, TypeName) :: declarations; // translate monitor invariant declarations = declarations ::: translateMonitorInvariant(cl.Invariants, cl.pos); // translate each member @@ -567,7 +567,7 @@ class Translator { } ::: // 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") ::: + (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") ::: // create a new token BLocal(tokenV) :: Havoc(tokenId) :: bassume(nonNull(tokenId)) :: // the following assumes help in proving that the token is fresh @@ -625,7 +625,7 @@ class Translator { 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) ::: + { p => SubstVars(p, Some(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) => @@ -648,7 +648,7 @@ class Translator { new Boogie.MapUpdate(etran.Credits, TrExpr(ch), new Boogie.MapSelect(etran.Credits, TrExpr(ch)) + 1) :: // exhale where clause Exhale(List( - (SubstThisAndVars(channel.where, formalThis, channel.parameters, formalParams), + (SubstVars(channel.where, Some(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) => @@ -672,7 +672,7 @@ class Translator { (formalThis := ch) :: (for (v <- formalParams) yield Havoc(v)) ::: // inhale where clause - Inhale(List(SubstThisAndVars(channel.where, formalThis, channel.parameters, formalParams)), "channel where clause") ::: + Inhale(List(SubstVars(channel.where, Some(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 @@ -808,14 +808,14 @@ class Translator { (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") ::: + (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") ::: // 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) ::: + LockHavoc(for (e <- LockChanges(c.m.spec) map (p => SubstVars(p, Some(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) ::: + (p => SubstVars(p, Some(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 @@ -834,9 +834,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, w.LoopTargetsList, + val lkchOld = lkch map (e => SubstVars(e, None, w.LoopTargetsList, for (v <- saveLocalsV) yield new VariableExpr(v))) - val lkchIterStart = lkch map (e => SubstVars(e, w.LoopTargetsList, + val lkchIterStart = lkch map (e => SubstVars(e, None, 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)) @@ -1186,7 +1186,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=> (SubstThisAndVars(pre, 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, Some(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 @@ -1259,10 +1259,10 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.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, q.variables, newVars map {v => At(seq, new VariableExpr(v)) })) + 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, q.variables, newVars map {v => At(seq, new VariableExpr(v)) })) + 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) } @@ -1298,7 +1298,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E var assumption2 = assumption; for(i <- is) { val iTmp = new Variable(i.UniqueName, new Type(IntClass)); - iTmps = iTmps + iTmp; + iTmps = iTmp :: iTmps; assumption2 = assumption2 && (Tr(min)<=VarExpr(iTmp.UniqueName)) && (VarExpr(iTmp.UniqueName) < Tr(max)) } // check definedness of the bounds @@ -1308,7 +1308,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E 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, is, iTmps map { iTmp => new VariableExpr(iTmp)}))(assumption2) + isDefined(SubstVars(e, None, is, iTmps map { iTmp => new VariableExpr(iTmp)}))(assumption2) } def Tr(e: Expression): Boogie.Expr = e match { @@ -1441,11 +1441,11 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.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, q.variables, is map {v => At(seq, new VariableExpr(v))}); + 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, q.variables, is map {v => At(seq, new VariableExpr(v))}); + 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; @@ -1767,7 +1767,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case CallState(token, obj, id, args) => val argsSeq = CallArgs(Heap.select(Tr(token), "joinable")); - var i : int = 0; + var i = 0; (CallHeap(Heap.select(Tr(token), "joinable")), CallMask(Heap.select(Tr(token), "joinable")), CallCredits(Heap.select(Tr(token), "joinable")), @@ -1999,7 +1999,7 @@ object TranslationHelper { // implicit conversions implicit def bool2Bool(b: Boolean): Boogie.BoolLiteral = Boogie.BoolLiteral(b) - implicit def int2Int(n: int): Boogie.IntLiteral = Boogie.IntLiteral(n) + 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; @@ -2154,20 +2154,20 @@ object TranslationHelper { } else { if(ma.isPredicate){ // assumption: obj!=null - (assumptions ::: Neq(obj, NullLiteral()) :: Nil, handled1 + ma) + (assumptions ::: Neq(obj, NullLiteral()) :: Nil, handled1 ::: List(ma)) } else { // assumption: obj!=null && acc(obj, f) - (assumptions ::: Neq(obj, NullLiteral()) :: Access(ma, None) :: Nil, handled1 + ma) + (assumptions ::: Neq(obj, NullLiteral()) :: Access(ma, None) :: Nil, handled1 ::: List(ma)) } } case Access(ma@MemberAccess(obj, f), perm) => - val (assumptions, handled1) = automagic(obj, handled + ma); + val (assumptions, handled1) = automagic(obj, handled ::: List(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); + val (assumptions, handled1) = automagic(obj, handled ::: List(ma)); perm match { case None => (assumptions, handled1); case Some(None) => (assumptions, handled1); @@ -2277,7 +2277,7 @@ object TranslationHelper { 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) + SubstVars(func.f.definition, Some(obj), func.f.ins, args) case _ => manipulate(e, {ex => unfoldPred(ex)}) } } @@ -2285,22 +2285,32 @@ object TranslationHelper { } // needed to do a _simultaneous_ substitution! - def SubstThisAndVars(expr: Expression, thisReplacement: Expression, vs: List[Variable], xs: List[Expression]): Expression = { - def replace(e: Expression): Expression = { + 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 + case _: ThisExpr => + thisReplacement match { + case Some(e) => e; + case None => e; + } case e: VariableExpr => - for ((v,x) <- vs zip xs if v == e.v) { return x } + for ((v,x) <- sub 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})); + 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)}) + case _ => manipulate(e, {ex => replace(ex, sub)}) } } - replace(expr) + replace(expr, vs zip xs) } def SubstThis(expr: Expression, x: Expression): Expression = { @@ -2323,23 +2333,7 @@ object TranslationHelper { 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) - } - + /** 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 @@ -2389,6 +2383,7 @@ object TranslationHelper { 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)=> @@ -2403,6 +2398,8 @@ object TranslationHelper { 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)) -- cgit v1.2.3