Chalice: Changed definition of waitlevel to take into account rdlock. Adapted definition of IsGoodInhaleState and an axiom.

2 files changed, 4 insertions, 3 deletions

diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala
index 3dcc0ccb..2fb58697 100644
--- a/Chalice/src/Prelude.scala
+++ b/Chalice/src/Prelude.scala
@@ -97,7 +97,8 @@ function IsGoodInhaleState(ih: HeapType, h: HeapType,
   (forall<T> o: ref, f: Field T :: { ih[o, f] }  CanRead(m, o, f) ==> ih[o, f] == h[o, f]) &&

   (forall o: ref :: { ih[o, held] }  (0<ih[o, held]) == (0<h[o, held])) &&

   (forall o: ref :: { ih[o, rdheld] }  ih[o, rdheld] == h[o, rdheld]) &&

-  (forall o: ref :: { h[o, held] }  (0<h[o, held]) ==> ih[o, mu] == h[o, mu])

+  (forall o: ref :: { h[o, held] }  (0<h[o, held]) ==> ih[o, mu] == h[o, mu]) &&

+  (forall o: ref :: { h[o, rdheld] }  h[o, rdheld] ==> ih[o, mu] == h[o, mu])

 }

 

 function ite<T>(bool, T, T) returns (T);

@@ -199,7 +200,7 @@ function Seq#Range(min: int, max: int) returns (Seq int);
 axiom (forall min: int, max: int :: { Seq#Length(Seq#Range(min, max)) } (min < max ==> Seq#Length(Seq#Range(min, max)) == max-min) && (max <= min ==> Seq#Length(Seq#Range(min, max)) == 0));

 axiom (forall min: int, max: int, j: int :: { Seq#Index(Seq#Range(min, max), j) } 0<=j && j<max-min ==> Seq#Index(Seq#Range(min, max), j) == min + j);

 

-axiom (forall h: HeapType, m: MaskType, o: ref, q: ref :: {wf(h, m), h[o, mu], h[q, mu]} wf(h, m) && o!=q && (0 < h[o, held]) && (0 < h[q, held]) ==> h[o, mu] != h[q, mu]);

+axiom (forall h: HeapType, m: MaskType, o: ref, q: ref :: {wf(h, m), h[o, mu], h[q, mu]} wf(h, m) && o!=q && (0 < h[o, held] || h[o, rdheld]) && (0 < h[q, held] || h[q, rdheld]) ==> h[o, mu] != h[q, mu]);

 

 function DecPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);

 

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 7a85ef74..644d203c 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -1966,7 +1966,7 @@ object TranslationHelper {
   def IsGoodMask(m: Expr) = FunctionApp("IsGoodMask", List(m))

   def IsGoodInhaleState(a: Expr, b: Expr, c: Expr) = FunctionApp("IsGoodInhaleState", List(a, b, c))

   def contributesToWaitLevel(e: Expr, h: Expr, c: Expr) =

-    (0 < h.select(e, "held")) || (new Boogie.MapSelect(c, e) < 0)

+    (0 < h.select(e, "held")) || h.select(e, "rdheld")  || (new Boogie.MapSelect(c, e) < 0)

   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)))