summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Chalice/refinements/original/Counter.chalice128
-rw-r--r--Chalice/src/Ast.scala4
-rw-r--r--Chalice/src/Parser.scala22
-rw-r--r--Chalice/src/Resolver.scala19
-rw-r--r--Chalice/src/Translator.scala28
5 files changed, 41 insertions, 160 deletions
diff --git a/Chalice/refinements/original/Counter.chalice b/Chalice/refinements/original/Counter.chalice
deleted file mode 100644
index 310a9d78..00000000
--- a/Chalice/refinements/original/Counter.chalice
+++ /dev/null
@@ -1,128 +0,0 @@
-class Cell {var n: int;}
-
-class Counter0 {
- var x: int;
-
- method init()
- requires acc(this.*);
- ensures acc(x);
- {
- x := 0;
- }
-
- method inc()
- requires acc(x);
- ensures acc(x);
- {
- x := x + 1;
- }
-
- method dec()
- requires acc(x);
- ensures acc(x);
- {
- x := x - 1;
- }
-
- method magic1() returns (c: Cell)
- requires acc(x)
- ensures acc(c.n);
- {
- c := new Cell;
- }
-
- method magic2() returns (c: Cell)
- requires acc(x);
- ensures acc(x) && acc(c.n);
- {
- c := new Cell;
- }
-}
-
-class Counter1 {
- ghost var x: int;
- var y: int;
- var z: int;
- // replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
-
- method init()
- requires acc(this.*);
- ensures acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
- {
- x := 0;
- y := 0;
- z := 0;
- }
-
- method inc()
- requires acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
- ensures acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
- {
- x := x + 1;
- y := y + 1;
- }
-
- method dec()
- requires acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
- ensures acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
- {
- x := x - 1;
- z := z + 1;
- }
-}
-
-class Counter2 {
- ghost var x: int;
- ghost var y: int;
- ghost var z: int;
- var a: Cell;
- var b: Cell;
- // replace y || z by acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
-
- method init()
- requires acc(this.*);
- ensures acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
- {
- x := 0;
- y := 0;
- z := 0;
- a := new Cell;
- b := new Cell;
- a.n := 0;
- b.n := 0;
- }
-
- method inc()
- requires acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
- ensures acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
- {
- x := x + 1;
- y := y + 1;
- a.n := a.n + 1;
- }
-
- method dec()
- requires acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
- ensures acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
- {
- x := x - 1;
- z := z + 1;
- b.n := b.n + 1;
- }
-
- method magic1() returns (c: Cell)
- requires acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
- ensures acc(c.n);
- {
- c := a;
- }
-
- method magic2() returns (c: Cell)
- requires acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
- ensures acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n && acc(c.n);
- {
- c := a;
- }
-}
-
-
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 82391a9c..4e30c621 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -38,6 +38,8 @@ sealed case class Class(classId: String, parameters: List[Class], module: String
def LookupMember(id: String): Option[NamedMember] = {
if (id2member contains id)
Some(id2member(id))
+ else if (IsRefinement)
+ refines.LookupMember(id)
else if (IsRef && this != RootClass) {
// check with root class
RootClass LookupMember id match {
@@ -187,7 +189,7 @@ case class LockChange(ee: List[Expression]) extends Specification
case class CouplingInvariant(ids: List[String], e: Expression) extends Member {
assert(ids.size > 0)
- var fields = null:List[Field]
+ var fields = Nil:List[Field]
}
case class MethodTransform(id: String, ins: List[Variable], outs: List[Variable], spec: List[Specification], trans: Transform) extends Callable(id) {
var refines = null: Callable
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 0aaef3f0..36f0e22b 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -71,14 +71,14 @@ class Parser extends StandardTokenParsers {
*/
def memberDecl = {
- currentLocalVariables = Set[String](); assumeAllLocals = false;
- positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl | predicateDecl | functionDecl | transformDecl | couplingDecl)
+ currentLocalVariables = Set[String]();
+ positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl | predicateDecl | functionDecl | couplingDecl | transformDecl) // important that last one is transformDecl
}
def fieldDecl =
( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, false) }
| "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, true) }
)
- def invariantDecl = positioned("invariant" ~> expression <~ Semi ^^ MonitorInvariant)
+ def invariantDecl = "invariant" ~> expression <~ Semi ^^ MonitorInvariant
def methodDecl =
"method" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~
(methodSpec*) ~ blockStatement ^^ {
@@ -96,16 +96,16 @@ class Parser extends StandardTokenParsers {
"condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ {
case id ~ optE => Condition(id, optE) }
def transformDecl = {
- assumeAllLocals = true;
- "transforms" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~
- (methodSpec*) ~ ("{" ~> transform <~ "}") ^^ {
- case id ~ ins ~ outs ~ spec ~ trans =>
- MethodTransform(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, AST.normalize(trans))
+ "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 couplingDecl = positioned(
- ("replaces" ~> rep1(ident) <~ "by") ~ expression <~ Semi ^^ {case ids ~ e => CouplingInvariant(ids, e)}
- )
+ def couplingDecl = ("replaces" ~> rep1sep(ident, ",") <~ "by") ~ expression <~ Semi ^^ {case ids ~ e => CouplingInvariant(ids, e)}
def formalParameters(immutable: Boolean) =
"(" ~> (formalList(immutable) ?) <~ ")" ^^ {
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 19ae2bbd..bdcc7108 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -86,15 +86,16 @@ object Resolver {
case cl: Class if cl.IsRefinement =>
if (! (decls contains cl.refinesId)) {
return Errors(List((cl.pos, "refined class " + cl.refinesId + " does not exist")))
- } else if (! decls(cl.refinesId).isInstanceOf[Class]) {
- return Errors(List((cl.pos, "refined declaration " + cl.refinesId + " is not a class")))
} else if (cl.refinesId == cl.id) {
return Errors(List((cl.pos, "class cannot refine itself")))
- } else {
- cl.refines = decls(cl.refinesId).asInstanceOf[Class];
- refinesRel.addNode(cl);
- refinesRel.addNode(cl.refines);
- refinesRel.addEdge(cl, cl.refines);
+ } else decls(cl.refinesId) match {
+ case abs: Class =>
+ cl.refines = abs;
+ refinesRel.addNode(cl);
+ refinesRel.addNode(cl.refines);
+ refinesRel.addEdge(cl, cl.refines);
+ case _ =>
+ return Errors(List((cl.pos, "refined declaration " + cl.refinesId + " is not a class")))
}
case _ =>
}
@@ -224,7 +225,8 @@ object Resolver {
}
case None =>
}
- case mt: MethodTransform =>
+ case mt: MethodTransform => // need to resolve them in reverse refinement order
+ case ci: CouplingInvariant => ResolveCouplingInvariant(ci, cl, baseContext)
}
}
}
@@ -242,7 +244,6 @@ object Resolver {
for (List(cl) <- dag.computeTopologicalSort.reverse) {
for (m <- cl.members) m match {
case mt: MethodTransform => ResolveTransform(mt, baseContext)
- case ci: CouplingInvariant => ResolveCouplingInvariant(ci, cl, baseContext)
case _ =>
}
}
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 75d23e53..915049b2 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -23,7 +23,8 @@ class Translator {
def translateProgram(decls: List[TopLevelDecl]): List[Decl] = {
decls flatMap {
case cl: Class => translateClass(cl)
- case ch: Channel => translateClass(ChannelClass(ch)) /* TODO: admissibility check of where clause */
+ case ch: Channel => translateClass(ChannelClass(ch))
+ /* TODO: admissibility check of where clause */
/* TODO: waitlevel not allowed in postcondition of things forked (or, rather, joined) */
}
}
@@ -68,6 +69,8 @@ class Translator {
throw new Exception("not yet implemented")
case mt: MethodTransform =>
translateMethodTransform(mt)
+ case ci: CouplingInvariant =>
+ Nil
}
}
@@ -139,15 +142,17 @@ class Translator {
ExhaleWithChecking(Postconditions(f.spec) map { post => ((if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(post) else post),
ErrorMessage(f.pos, "Postcondition at " + post.pos + " might not hold."))}, "function postcondition")) ::
// definition axiom
- (if (f.definition.isDefined) definitionAxiom(f) else Nil) :::
+ (f.definition match {
+ case Some(definition) => definitionAxiom(f, definition);
+ case None => Nil
+ }) :::
// framing axiom (+ frame function)
framingAxiom(f) :::
// postcondition axiom(s)
postconditionAxiom(f)
}
- def definitionAxiom(f: Function): List[Decl] = {
- assert(f.definition.isDefined)
+ def definitionAxiom(f: Function, definition: Expression): List[Decl] = {
val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
val args = VarExpr("this") :: inArgs;
val formals = BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar);
@@ -157,7 +162,7 @@ class Translator {
val body = etran.Tr(
if (f.isRecursive && ! f.isUnlimited) {
val limited = Map() ++ (f.SCC zip (f.SCC map {f =>
- val result = Function(f.id + "#limited", f.ins, f.out, f.spec, f.definition);
+ val result = Function(f.id + "#limited", f.ins, f.out, f.spec, None);
result.Parent = f.Parent;
result;
}));
@@ -168,9 +173,9 @@ class Translator {
Some(result)
case _ => None
}
- f.definition.get transform limit;
+ definition transform limit;
} else {
- f.definition.get
+ definition
}
);
@@ -221,7 +226,7 @@ class Translator {
(applyF ==@ applyFrameFunction))
)
} else {
- // Encoding with two heap quantification
+ // Encoding with universal quantification over two heaps
/* axiom (forall h1, h2: HeapType, m1, m2: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::
wf(h1,m1) && wf(h2,m2) && version(h1, h2, #C.f) ==>
#C.f(h1, m1, this, x_1, ..., x_n) == #C.f(h2, m2, this, x_1, ..., x_n)
@@ -247,8 +252,7 @@ class Translator {
}
def postconditionAxiom(f: Function): List[Decl] = {
- /* function ##C.f(state, ref, t_1, ..., t_n) returns (t);
- axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::
+ /* axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::
wf(h, m) && CanAssumeFunctionDefs ==> Q[#C.f(h, m, this, x_1, ..., x_n)/result]
*/
val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
@@ -2459,7 +2463,7 @@ object TranslationHelper {
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 && func.f.definition.isDefined =>
+ case func@FunctionApplication(obj: ThisExpr, name, args) if 2<=Chalice.defaults && func.f.definition.isDefined =>
Some(SubstVars(func.f.definition.get, obj, func.f.ins, args))
case _ => None
}
@@ -2563,7 +2567,9 @@ object TranslationHelper {
}
}
+ // tags statements to be preserved
val keepTag = Boogie.Tag("keep")
+
// Assume the only composite statement in Boogie is If
def tag(l: List[Stmt], t: Boogie.Tag):List[Stmt] =
for (s <- l) yield {
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 12:03:35 +0000