From 747f201231e03caee7289d03b1e2a29dacae7635 Mon Sep 17 00:00:00 2001 From: kyessenov Date: Sun, 22 Aug 2010 06:43:51 +0000 Subject: Chalice: * coupling invariants work (with certain restrictions as described in TODO comments) --- Chalice/refinements/Answer | 6 ++ Chalice/refinements/Counter.chalice | 125 +++++++++++++++++++++++++++++++ Chalice/refinements/TestCoupling.chalice | 74 ++++++++++++++++++ Chalice/refinements/test.sh | 1 + Chalice/src/Ast.scala | 21 +++++- Chalice/src/Parser.scala | 27 +++---- Chalice/src/PrettyPrinter.scala | 31 ++++++-- Chalice/src/Resolver.scala | 4 +- Chalice/src/Translator.scala | 56 ++++++++++---- 9 files changed, 305 insertions(+), 40 deletions(-) create mode 100644 Chalice/refinements/Counter.chalice create mode 100644 Chalice/refinements/TestCoupling.chalice (limited to 'Chalice') diff --git a/Chalice/refinements/Answer b/Chalice/refinements/Answer index b513e041..6db2a988 100644 --- a/Chalice/refinements/Answer +++ b/Chalice/refinements/Answer @@ -29,3 +29,9 @@ Processing Pick.chalice 26.25: Sequence index might be larger than or equal to the length of the sequence. Boogie program verifier finished with 11 verified, 1 error +Processing TestCoupling.chalice + 35.13: The postcondition at 35.13 might not hold. Insufficient fraction at 35.13 for A1.y. + 62.38: Location might not be readable. + 66.5: Location might not be writable + +Boogie program verifier finished with 17 verified, 3 errors diff --git a/Chalice/refinements/Counter.chalice b/Chalice/refinements/Counter.chalice new file mode 100644 index 00000000..c9576a13 --- /dev/null +++ b/Chalice/refinements/Counter.chalice @@ -0,0 +1,125 @@ +class Counter0 { + var x: int; + + method init() + requires acc(x); + ensures acc(x) && x == 0; + { + x := 0; + } + + method inc() + requires acc(x); + ensures acc(x) && x == old(x) + 1; + { + x := x + 1; + } + + method dec() + requires acc(x); + ensures acc(x) && x == old(x) - 1; + { + x := x - 1; + } + + /** Interesting issues */ + + /* We can expose representation here */ + method magic1() returns (c: Cell) + requires acc(x) + ensures acc(c.n) && x == old(x); + { + var c [acc(c.n)]; + } + + /* This should prevent us from exposing representation */ + method magic2() returns (c: Cell) + requires acc(x); + ensures acc(x) && x == old(x) && acc(c.n); + { + var c [acc(c.n)]; + } +} + +class Counter1 refines Counter0 { + var y: int; + var z: int; + replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0; + + transforms init() + { + replaces * by {this.y := 0; this.z := 0;} + } + + transforms inc() + { + replaces * by {this.y := this.y + 1;} + } + + transforms dec() + { + replaces * by {this.z := this.z + 1;} + } + + /** This violates abstraction of x -- we must hold all permissions to x to update it */ + method magic3() + requires acc(y); + { + y := y + 1; + } + + /** This does also -- but it also prohibits us from reading part of the state across refinement */ + method magic4() returns (i) + requires acc(y); + { + i := y; + } +} + +class Cell {var n: int} +/* +class Counter2 refines Counter1 { + var a: Cell; + var b: Cell; + replaces y, z by acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n; + + transforms init() + { + replaces * by { + this.a := new Cell {n := 0}; + this.b := new Cell {n := 0}; + } + } + + transforms inc() + { + replaces * by {this.a.n := this.a.n + 1;} + } + + transforms dec() + { + replaces * by {this.b.n := this.b.n + 1;} + } + + transforms magic1() returns (c: Cell) + { + replaces * by {c := this.a;} + } + + transforms magic2() returns (c: Cell) + { + replaces * by {c := this.a;} + } + + transforms magic3() + { + replaces * by {this.a.n := this.a.n + 1;} + } + + transforms magic4() returns (i) + { + replaces * by {i := this.a.n;} + } +} +*/ + diff --git a/Chalice/refinements/TestCoupling.chalice b/Chalice/refinements/TestCoupling.chalice new file mode 100644 index 00000000..a178c9b4 --- /dev/null +++ b/Chalice/refinements/TestCoupling.chalice @@ -0,0 +1,74 @@ +class A0 { + var x: int; + var n: int; + var k: int; + + method inc() + requires acc(x) && acc(n); + ensures acc(x) && x == old(x) + 1; + { + x := x + 1; + n := n + 1; + } + + method error() + requires acc(x) + ensures acc(x) + { + x := x + 1; + } +} + +class A1 refines A0 { + var y: int; + var z: int; + replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0; + + refines inc() + ensures y == old(y) + 1 + { + this.y := 1 + this.y; + this.n := this.n + 1; + } + + refines error() + ensures acc(y) + { + this.y := 1 + this.y; + } +} + +class B0 { + var x: int; + var y: int; + + method error() + requires acc(x); + ensures acc(x); + { + x := x + 1; + } + + method inc() + requires acc(x) && acc(y); + ensures acc(x) && acc(y); + { + x := x + 1; + } +} + +class B1 refines B0 { + var z: int; + replaces x,y by acc(z) && z == x + y; + + refines error() + { + this.z := this.z + 1; + } + + refines inc() + { + this.z := this.z + 1; + } +} + diff --git a/Chalice/refinements/test.sh b/Chalice/refinements/test.sh index 73ede390..24dbd6e5 100644 --- a/Chalice/refinements/test.sh +++ b/Chalice/refinements/test.sh @@ -13,6 +13,7 @@ TESTS=" RecFiniteDiff.chalice LoopFiniteDiff.chalice Pick.chalice + TestCoupling.chalice " # Switch to test directory diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala index 4e30c621..92c339ea 100644 --- a/Chalice/src/Ast.scala +++ b/Chalice/src/Ast.scala @@ -28,10 +28,12 @@ sealed case class Class(classId: String, parameters: List[Class], module: String def IsState: Boolean = false def IsNormalClass = true - lazy val Fields: List[Field] = members flatMap {case x: Field => List(x); case _ => Nil} + lazy val DeclaredFields = members flatMap {case x: Field => List(x); case _ => Nil} lazy val MentionableFields = Fields filter {x => ! x.Hidden} - lazy val Invariants: List[MonitorInvariant] = members flatMap {case x: MonitorInvariant => List(x); case _ => Nil} - lazy val id2member:Map[String,NamedMember] = Map() ++ { + lazy val MonitorInvariants = members flatMap {case x: MonitorInvariant => List(x); case _ => Nil} + lazy val Fields:List[Field] = DeclaredFields ++ (if (IsRefinement) refines.Fields else Nil) + + private lazy val id2member:Map[String,NamedMember] = Map() ++ { val named = members flatMap {case x: NamedMember => List(x); case _ => Nil}; (named map {x => x.Id}) zip named } @@ -59,6 +61,8 @@ sealed case class Class(classId: String, parameters: List[Class], module: String var IsRefinement = false var refinesId: String = null var refines: Class = null + lazy val CouplingInvariants = members flatMap {case x: CouplingInvariant => List(x); case _ => Nil} + lazy val Replaces: List[Field] = CouplingInvariants flatMap (_.fields) } sealed case class Channel(channelId: String, parameters: List[Variable], where: Expression) extends TopLevelDecl(channelId) @@ -190,6 +194,13 @@ case class LockChange(ee: List[Expression]) extends Specification case class CouplingInvariant(ids: List[String], e: Expression) extends Member { assert(ids.size > 0) var fields = Nil:List[Field] + /* Distribute 100 between fields */ + def fraction(field: Field) = { + val k = fields.indexOf(field) + assert (0 <= k && k < fields.size) + val part: Int = 100 / fields.size + if (k == fields.size - 1) IntLiteral(100 - part * k) else IntLiteral(part) + } } case class MethodTransform(id: String, ins: List[Variable], outs: List[Variable], spec: List[Specification], trans: Transform) extends Callable(id) { var refines = null: Callable @@ -229,7 +240,9 @@ case class BlockPat() extends Transform { /** Matches any block of code (greedily) and acts as identity */ case class SkipPat() extends Transform /** Replacement pattern for arbitrary block */ -case class ProgramPat(code: List[Statement]) extends Transform +case class ProgramPat(code: List[Statement]) extends Transform { + if (code.size > 0) pos = code.first.pos +} case class IfPat(thn: Transform, els: Option[Transform]) extends Transform case class WhilePat(invs: List[Expression], body: Transform) extends Transform case class NonDetPat(is: List[String], code: List[Statement]) extends Transform { diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index 36f0e22b..d12ca00f 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -83,9 +83,8 @@ class Parser extends StandardTokenParsers { "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) }} + Method(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, body) + } def predicateDecl: Parser[Predicate] = ("predicate" ~> ident) ~ ("{" ~> expression <~ "}") ^^ { case id ~ definition => Predicate(id, definition) } def functionDecl = @@ -95,16 +94,18 @@ class Parser extends StandardTokenParsers { def conditionDecl = "condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ { case id ~ optE => Condition(id, optE) } - def transformDecl = { - "transforms" ~> ident into {id => - assumeAllLocals = true; - formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~ (methodSpec*) ~ ("{" ~> transform <~ "}") ^^ { - case ins ~ outs ~ spec ~ trans => - assumeAllLocals = false; - MethodTransform(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, AST.normalize(trans)) - } - } - } + def transformDecl = + ( "refines" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~ (methodSpec*) ~ blockStatement ^^ { + case id ~ ins ~outs ~ spec ~ body => + MethodTransform(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, ProgramPat(body)) }).|( + "transforms" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~ (methodSpec*) into {case id ~ ins ~ outs ~ spec => + assumeAllLocals = true; + "{" ~> transform <~ "}" ^^ { + trans => + assumeAllLocals = false; + MethodTransform(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, AST.normalize(trans)) + } + }) def couplingDecl = ("replaces" ~> rep1sep(ident, ",") <~ "by") ~ expression <~ Semi ^^ {case ids ~ e => CouplingInvariant(ids, e)} def formalParameters(immutable: Boolean) = diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala index da96c796..b2f30c5c 100644 --- a/Chalice/src/PrettyPrinter.scala +++ b/Chalice/src/PrettyPrinter.scala @@ -8,7 +8,8 @@ object PrintProgram { def P(prog: List[TopLevelDecl]) = for (decl <- prog) decl match { case cl: Class => - if (cl.IsExternal) print("external ") + if (cl.IsExternal) + print("external ") println("class " + cl.id + " module " + cl.module + (if (cl.IsRefinement) " refines " + cl.refinesId else "") + " {") cl.members foreach Member println("}") @@ -24,11 +25,15 @@ object PrintProgram { case m: Method => print(" method " + m.id) print("("); VarList(m.ins); print(")") - if (m.outs != Nil) print(" returns ("); VarList(m.outs); print(")") + if (m.outs != Nil) { + print(" returns ("); VarList(m.outs); print(")") + } println PrintSpec(m.Spec) println(" {") - for (s <- m.body) {Spaces(4); Stmt(s, 4)} + for (s <- m.body) { + Spaces(4); Stmt(s, 4) + } println(" }") case Condition(id, optE) => print(" condition " + id) @@ -50,14 +55,18 @@ object PrintProgram { case m: MethodTransform => print(" method " + m.id); print("("); VarList(m.ins); print(")") - if (m.outs != Nil) print(" returns ("); VarList(m.outs); print(")") + if (m.outs != Nil) { + print(" returns ("); VarList(m.outs); print(")") + } println; if (m.refines != null) PrintSpec(m.Spec); println(" {"); if (m.body == null) println(" // body transform is not resolved") else - for (s <- m.body) {Spaces(4); Stmt(s, 4)} + for (s <- m.body) { + Spaces(4); Stmt(s, 4) + } println(" }") case CouplingInvariant(ids, e) => print(" replaces "); Commas(ids); print(" by "); Expr(e); println(Semi); @@ -79,9 +88,13 @@ object PrintProgram { PrintBlockStmt(ss, indent); println case RefinementBlock(ss, old) => println("/* begin of refinement block") - for (s <- old) {Spaces(indent + 2); Stmt(s, indent + 2)} + for (s <- old) { + Spaces(indent + 2); Stmt(s, indent + 2) + } Spaces(indent); println("end of abstract code */") - for (s <- ss) {Spaces(indent); Stmt(s, indent)} + for (s <- ss) { + Spaces(indent); Stmt(s, indent) + } Spaces(indent); println("// end of refinement block") case IfStmt(guard, BlockStmt(thn), els) => print("if ("); Expr(guard); print(") ") @@ -207,7 +220,9 @@ object PrintProgram { } def PrintBlockStmt(ss: List[Statement], indent: Int) = { println("{") - for (s <- ss) { Spaces(indent+2); Stmt(s, indent+2) } + for (s <- ss) { + Spaces(indent+2); Stmt(s, indent+2) + } Spaces(indent); print("}") } def VarList(vv: List[Variable]) = Commas(vv map {v => v.id + ": " + v.t.FullName}) diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala index bdcc7108..d4adbec3 100644 --- a/Chalice/src/Resolver.scala +++ b/Chalice/src/Resolver.scala @@ -1079,7 +1079,7 @@ object Resolver { def ResolveTransform(mt: MethodTransform, context: ProgramContext) { mt.spec foreach { case Precondition(e) => - context.Error(e.pos, "Method refinement cannot have a pre-condition") + context.Error(e.pos, "Method refinement cannot add a pre-condition") case Postcondition(e) => ResolveExpr(e, context.SetClass(mt.Parent).SetMember(mt), true, true)(false) case _ : LockChange => throw new Exception("not implemented") @@ -1139,5 +1139,7 @@ object Resolver { } ResolveExpr(ci.e, context.SetClass(cl).SetMember(ci), false, true)(true) if (!ci.e.typ.IsBool) context.Error(ci.pos, "coupling invariant requires a boolean expression (found " + ci.e.typ.FullName + ")") + // TODO: check coupling invariant may only give permissions to newly declared fields + // TODO: check concrete body cannot refer to replaced fields } } diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 915049b2..ef27e635 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -41,7 +41,7 @@ class Translator { // add class name declarations = Const(className(cl).id, true, TypeName) :: declarations; // translate monitor invariant - declarations = declarations ::: translateMonitorInvariant(cl.Invariants, cl.pos); + declarations = declarations ::: translateMonitorInvariant(cl.MonitorInvariants, cl.pos); // translate each member for(member <- cl.members) { declarations = declarations ::: translateMember(member); @@ -323,6 +323,20 @@ class Translator { } def translateMethodTransform(mt: MethodTransform): List[Decl] = { + // extract coupling invariants + def Invariants(e: Expression): Expression = desugar(e) match { + case And(a,b) => And(Invariants(a), Invariants(b)) + case Implies(a,b) => Implies(a, Invariants(b)) + case Access(ma, Full) if ! ma.isPredicate => + val cis = for (ci <- mt.Parent.CouplingInvariants; if (ci.fields.contains(ma.f))) yield FractionOf(ci.e, ci.fraction(ma.f)); + cis.foldLeft(BoolLiteral(true):Expression)(And(_,_)) + case _: PermissionExpr => throw new Exception("not supported") + case _ => BoolLiteral(true) + } + + val preCI = if (mt.Parent.CouplingInvariants.size > 0) Preconditions(mt.Spec).map(Invariants) else Nil + val postCI = if (mt.Parent.CouplingInvariants.size > 0) Postconditions(mt.refines.Spec).map(Invariants) else Nil + // check definedness of refinement specifications Proc(mt.FullName + "$checkDefinedness", NewBVarWhere("this", new Type(currentClass)) :: (mt.Ins map {i => Variable2BVarWhere(i)}), @@ -332,12 +346,13 @@ class Translator { DefinePreInitialState ::: bassume(CanAssumeFunctionDefs) :: // check precondition - InhaleWithChecking(Preconditions(mt.Spec), "precondition") ::: + InhaleWithChecking(Preconditions(mt.Spec) ::: preCI, "precondition") ::: DefineInitialState ::: (etran.Mask := ZeroMask) :: (etran.Credits := ZeroCredits) :: Havoc(etran.Heap) :: // check postcondition - InhaleWithChecking(Postconditions(mt.Spec), "postcondition") + InhaleWithChecking(Postconditions(mt.refines.Spec), "postcondition") ::: + tag(InhaleWithChecking(postCI ::: Postconditions(mt.spec), "postcondition"), keepTag) ) :: // check correctness of refinement Proc(mt.FullName, @@ -349,15 +364,16 @@ class Translator { bassume(CurrentModule ==@ Boogie.VarExpr(ModuleName(currentClass))) :: bassume(CanAssumeFunctionDefs) :: DefinePreInitialState ::: - Inhale(Preconditions(mt.Spec), "precondition") ::: + Inhale(Preconditions(mt.Spec) ::: preCI, "precondition") ::: DefineInitialState ::: translateStatements(mt.body) ::: Exhale(Postconditions(mt.refines.Spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition") ::: - tag( - Exhale(Postconditions(mt.spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}, "refinement postcondition"), - keepTag) + tag(Exhale( + (postCI map {p => (p, ErrorMessage(mt.pos, "The coupling invariant might not be preserved."))}) ::: + (Postconditions(mt.spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}), "postcondition"), keepTag) } ) + } def DebtCheck() = { @@ -1053,9 +1069,9 @@ class Translator { val afterV = for (v <- before) yield new Variable(v.id, v.t) Comment("refinement block") :: + // save heap (for (c <- conGlobals) yield BLocal(c)) ::: (for ((c, a) <- conGlobals zip etran.Globals) yield (new VarExpr(c) := a)) ::: - // TODO: inhale heap, global coupling: assume coupling invariant for locations with positive permission // save shared local variables (for (v <- beforeV) yield BLocal(Variable2BVarWhere(v))) ::: (for ((v, w) <- beforeV zip before) yield (new VariableExpr(v) := new VariableExpr(w))) ::: @@ -1071,7 +1087,7 @@ class Translator { r.abs match { case List(s: SpecStmt) => tag( - Comment("witness declared local variables") :: + Comment("give witnesses to declared local variables") :: (for (v <- duringA) yield BLocal(Variable2BVarWhere(v))) ::: (for ((v, w) <- duringA zip duringC) yield (new VariableExpr(v) := new VariableExpr(w))) ::: bassert(s.post, r.pos, "Refinement may fail to satisfy specification statement post-condition") :: @@ -1093,8 +1109,18 @@ class Translator { bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may produce different value for a declared local variable: " + v.id)), keepTag) }} ::: + { + val (v,ve) = NewBVar("this", tref, true) + // TODO: we only preserve concrete fields of "this" at the moment + // TODO: check for mask coupling + + // assert equality on shared globals (except those that are replaced) + (for (f <- currentClass.refines.Fields; if ! currentClass.CouplingInvariants.exists(_.fields.contains(f))) + yield bassert((absTran.Heap.select(ve, f.FullName) ==@ conTran.Heap.select(ve, f.FullName)).forall(v), r.pos, "Refinement may change value of field " + f.FullName)) ::: + // copy new globals from concrete to abstract heap (to preserve their values across refinement blocks and establish invariant) + (for (f <- currentClass.DeclaredFields) yield absTran.Heap.store(VarExpr("this"), VarExpr(f.FullName), conTran.Heap.select(VarExpr("this"), f.FullName))) + } ::: Comment("end of refinement block") - // TODO: global coupling: assert coupling invariants for locations with positive, preserve permissions? } @@ -1241,7 +1267,7 @@ class Translator { 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 + tran.Inhale(obj.typ.MonitorInvariants map (inv => SubstThis(inv.e, sh)) map (inv => (if (readonly) SubstRd(inv) else inv)), "monitor invariant", false) } @@ -1249,7 +1275,7 @@ class Translator { 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 + tran.Exhale(obj.typ.MonitorInvariants map (inv => SubstThis(inv.e, sh)) map (inv => (if (readonly) SubstRd(inv) else inv, msg)), "monitor invariant", false) } @@ -1257,7 +1283,7 @@ class Translator { 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 + Inhale(obj.typ.MonitorInvariants map (inv => SubstThis(inv.e, sh)) map (inv => (if (readonly) SubstRd(inv) else inv)), "monitor invariant") } @@ -1265,7 +1291,7 @@ class Translator { 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 + Exhale(obj.typ.MonitorInvariants map (inv => SubstThis(inv.e, sh)) map (inv => (if (readonly) SubstRd(inv) else inv, msg)), "monitor invariant") } @@ -2225,6 +2251,7 @@ object TranslationHelper { val result = expr match { case Access(e, Full) => Access(e, Frac(fraction)) case And(lhs, rhs) => And(FractionOf(lhs, fraction), FractionOf(rhs, fraction)) + case Implies(lhs, rhs) => Implies(lhs, FractionOf(rhs, fraction)) case _ if ! expr.isInstanceOf[PermissionExpr] => expr case _ => throw new Exception(" " + expr.pos + ": Scaling non-full permissions is not supported yet." + expr); } @@ -2236,6 +2263,7 @@ object TranslationHelper { expr match { case Access(e, Full) => true case And(lhs, rhs) => canTakeFractionOf(lhs) && canTakeFractionOf(rhs) + case Implies(lhs, rhs) => canTakeFractionOf(rhs) case _ if ! expr.isInstanceOf[PermissionExpr] => true case _ => false } -- cgit v1.2.3