summaryrefslogtreecommitdiff
path: root/Chalice
diff options
context:
space:
mode:
Diffstat (limited to 'Chalice')
-rw-r--r--Chalice/refinements/Answer6
-rw-r--r--Chalice/refinements/Counter.chalice125
-rw-r--r--Chalice/refinements/TestCoupling.chalice74
-rw-r--r--Chalice/refinements/test.sh1
-rw-r--r--Chalice/src/Ast.scala21
-rw-r--r--Chalice/src/Parser.scala27
-rw-r--r--Chalice/src/PrettyPrinter.scala31
-rw-r--r--Chalice/src/Resolver.scala4
-rw-r--r--Chalice/src/Translator.scala56
9 files changed, 305 insertions, 40 deletions
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
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 06:51:34 +0000