Chalice: No longer use Mask for "held" field; instead, only use the value of the "held" field in the heap

3 files changed, 10 insertions, 19 deletions

diff --git a/Chalice/examples/Answer b/Chalice/examples/Answer
index d9856d2d..e8ca406d 100644
--- a/Chalice/examples/Answer
+++ b/Chalice/examples/Answer
@@ -6,10 +6,10 @@ Boogie program verifier finished with 31 verified, 1 error
 ------ Running regression test counter.chalice 

   69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true.

   80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true.

-  119.5: The held field of the target of the release statement might not be writable.

+  119.5: The target of the release statement might be not be locked by the current thread.

   128.7: The mu field of the target of the acquire statement might not be above waitlevel.

   136.7: The mu field of the target of the acquire statement might not be above waitlevel.

-  145.5: The held field of the target of the release statement might not be writable.

+  145.5: The target of the release statement might be not be locked by the current thread.

 

 Boogie program verifier finished with 24 verified, 6 errors

 ------ Running regression test dining-philosophers.chalice 

@@ -181,8 +181,8 @@ The program did not typecheck.
   33.14: Location might not be readable.

   42.5: Monitor invariant might hot hold. The expression at 5.23 might not evaluate to true.

   60.5: Location might not be writable

-  76.5: The held field of the target of the unshare statement might not be writable.

-  84.5: The held field of the target of the unshare statement might not be writable.

+  76.5: The target of the unshare statement might not be shared.

+  84.5: The target of the unshare statement might not be shared.

 

 Boogie program verifier finished with 16 verified, 7 errors

 ------ Running regression test prog2.chalice 

@@ -201,10 +201,12 @@ Boogie program verifier finished with 24 verified, 4 errors
 Boogie program verifier finished with 51 verified, 4 errors

 ------ Running regression test prog4.chalice 

   5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true.

-  15.7: The held field of the target of the release statement might not be writable.

-  27.7: The held field of the target of the release statement might not be writable.

+  15.7: The target of the release statement might be not be locked by the current thread.

+  15.7: Release might fail because the current thread might hold the read lock.

+  27.7: The target of the release statement might be not be locked by the current thread.

+  27.7: Release might fail because the current thread might hold the read lock.

 

-Boogie program verifier finished with 6 verified, 3 errors

+Boogie program verifier finished with 6 verified, 5 errors

 ------ Running regression test ImplicitLocals.chalice 

 

 Boogie program verifier finished with 8 verified, 0 errors

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 4ce95b3e..14bd7d1c 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -671,7 +671,7 @@ object Resolver {
      if(inPredicate) context.Error(expr.pos, "holds cannot be mentioned in monitor invariants or predicates")

      if(! specContext)

        context.Error(expr.pos, "holds is allowed only in positive predicate contexts"); 

-     //todo: check that we are not in an invariant

+     //todo: check that we are not in a monitor invariant

      ResolveExpr(e, context, twoStateContext, false)

      expr.typ = BoolClass

    case expr@ RdHolds(e) =>

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 644d203c..10eafb6a 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -392,8 +392,6 @@ class Translator {
         bassert(nonNull(obj), s.pos, "The target of the share statement might be null.") ::

         UpdateMu(obj, true, false, lowerBounds, upperBounds, ErrorMessage(s.pos, "Share might fail.")) :::

         bassume(!isHeld(obj) && ! isRdHeld(obj)) :: // follows from o.mu==lockbottom

-        // no permission to o.held

-        etran.SetNoPermission(etran.Tr(obj), "held", etran.Mask) ::

         // exhale the monitor invariant (using the current state as the old state)

         ExhaleInvariants(obj, false, ErrorMessage(s.pos, "Monitor invariant might not hold."), etran.UseCurrentAsOld()) :::

         // assume a seen state is the one right before the share

@@ -407,15 +405,12 @@ class Translator {
         isDefined(obj) :::

         bassert(nonNull(o), s.pos, "The target of the unshare statement might be null.") ::

         bassert(CanWrite(o, "mu"), s.pos, "The mu field of the target of the unshare statement might not be writable.") ::

-        bassert(CanWrite(o, "held"), s.pos, "The held field of the target of the unshare statement might not be writable.") ::

         bassert(isShared(o), s.pos, "The target of the unshare statement might not be shared.") ::

         bassert(isHeld(o), s.pos, "The target of the unshare statement might not be locked by the current thread.") :: // locked or read-locked

         etran.Heap.store(o, "mu", bLockBottom) ::

         // havoc o.held where 0<=o.held 

         BLocal(heldV) :: Boogie.Havoc(held) :: bassume(held <= 0) ::

         etran.Heap.store(o, "held", held) ::

-        // set the permission of o.held to 0

-        etran.SetNoPermission(o, "held", etran.Mask) ::

         // set o.rdheld to false

         etran.Heap.store(o, "rdheld", false)

       case Acquire(obj) =>

@@ -729,7 +724,6 @@ class Translator {
     bassume(! isHeld(o) && ! isRdHeld(o)) :: // this assume follows from the previous assert

     // update the thread's locking state

     BLocal(lastAcquireVar) :: Havoc(lastAcquire) :: bassume(0 < lastAcquire) ::

-    etran.SetFullPermission(o, "held") ::

     etran.Heap.store(o, "held", lastAcquire) ::

     InhaleInvariants(nonNullObj, false, etran.WhereOldIs(

       LastSeenHeap(lastSeenMu, lastSeenHeld),

@@ -750,7 +744,6 @@ class Translator {
     BLocal(preReleaseHeapV) :: (preReleaseHeap := etran.Heap) ::

     BLocal(preReleaseMaskV) :: (preReleaseMask := etran.Mask) ::

     BLocal(preReleaseCreditsV) :: (preReleaseCredits := etran.Credits) ::

-    bassert(CanWrite(o, "held"), s.pos, "The held field of the target of the release statement might not be writable.") ::

     bassert(isHeld(o), s.pos, "The target of the release statement might be not be locked by the current thread.") ::

     bassert(!isRdHeld(o), s.pos, "Release might fail because the current thread might hold the read lock.") ::

     ExhaleInvariants(nonNullObj, false, ErrorMessage(s.pos, "Monitor invariant might hot hold."), etran.WhereOldIs(

@@ -760,7 +753,6 @@ class Translator {
     // havoc o.held where 0<=o.held 

     BLocal(heldV) :: Havoc(held) :: bassume(held <= 0) ::

     etran.Heap.store(o, "held", held) ::

-    etran.SetNoPermission(o, "held", etran.Mask) ::

     // assume a seen state is the one right before the share

     bassume(LastSeenHeap(etran.Heap.select(o, "mu"), held) ==@ preReleaseHeap) ::

     bassume(LastSeenMask(etran.Heap.select(o, "mu"), held) ==@ preReleaseMask) ::

@@ -1563,7 +1555,6 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
          isDefined(e)(true) :::

          bassert(nonNull(trE), holds.pos, "The target of the holds predicate might be null.")

        else Nil) :::

-      IncPermission(trE, "held", 100) :::

       bassume(IsGoodMask(Mask)) ::

       bassume(IsGoodState(Boogie.MapSelect(ih, trE, "held"))) ::

       bassume(wf(Heap, Mask)) ::

@@ -1709,10 +1700,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     case holds@Holds(e) => 

       (if(check) isDefined(e)(true) :::

       bassert(nonNull(Tr(e)), error.pos, error.message + " The target of the holds predicate at " + holds.pos + " might be null.") :: Nil else Nil) :::

-      bassert(HasFullPermission(Tr(e), "held", em), error.pos, error.message + " The current thread might not have full permission to the held field at " + holds.pos + ".") ::

       bassert(0 < Boogie.MapSelect(Heap, Tr(e), "held"), error.pos, error.message + " The current thread might not hold lock at " + holds.pos + ".") ::

       bassert(! Boogie.MapSelect(Heap, Tr(e), "rdheld"), error.pos, error.message + " The current thread might hold the read lock at " + holds.pos + ".") ::

-      SetNoPermission(Tr(e), "held", em) ::

       bassume(IsGoodMask(Mask)) ::

       bassume(wf(Heap, Mask)) ::

       bassume(wf(Heap, em))