Chalice: Fix a problem with permission expressions. Prevsiously, exhaling "acc(o.f,100-rd) && acc(o.f,rd)" resulted in a contradiction. This is now solved by using a two-step exhale (loosely speaking, read permissions and functional properties are exhaled first, and only afterwards all other permissions). Extended testcases appropriately.

3 files changed, 141 insertions, 84 deletions

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 8a9c690f..4233df85 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -1895,8 +1895,6 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   }

   

   def ExhalePermission(perm: Permission, obj: Expr, memberName: String, currentK: Expr, pos: Position, error: ErrorMessage, em: Boogie.Expr, exactchecking: Boolean): List[Boogie.Stmt] = {

-    val ec = needExactChecking(perm, exactchecking);

-    

     val (f, stmts) = extractKFromPermission(perm, currentK)

     val n = extractEpsilonsFromPermission(perm);

     

@@ -1904,13 +1902,13 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     (perm.permissionType match {

       case PermissionType.Mixed =>

         bassert(f > 0 || (f == 0 && n > 0), error.pos, error.message + " The permission at " + pos + " might not be positive.") ::

-        DecPermissionBoth(obj, memberName, f, n, em, error, pos, ec)

+        DecPermissionBoth(obj, memberName, f, n, em, error, pos, exactchecking)

       case PermissionType.Epsilons =>

         bassert(n > 0, error.pos, error.message + " The permission at " + pos + " might not be positive.") ::

         DecPermissionEpsilon(obj, memberName, n, em, error, pos)

       case PermissionType.Fraction =>

         bassert(f > 0, error.pos, error.message + " The permission at " + pos + " might not be positive.") ::

-        DecPermission(obj, memberName, f, em, error, pos, ec)

+        DecPermission(obj, memberName, f, em, error, pos, exactchecking)

     })

   }

   

@@ -1943,79 +1941,98 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     }

   }

   

-  def Exhale(p: Expression, em: Boogie.Expr, eh: Boogie.Expr, error: ErrorMessage, check: Boolean, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = desugar(p) match {

+  // Exhale is done in two passes: In the first run, everything except permissions

+  // which need exact checking are exhaled. Then, in the second run, those

+  // permissions are exhaled.

+  // The reason for this behaviour is that we want to support preconditions like

+  // "acc(o.f,100-rd) && acc(o.f,rd)", which should be equivalent to a full

+  // permission to o.f. However, when we exhale in the given order, we cannot

+  // use inexact checking for the abstract read permission ("acc(o.f,rd)"), as

+  // this would introduce the (unsound) assumption that "methodcallk < mask[o.f]".

+  // To avoid detecting this, we exhale all abstract read permissions first (or,

+  // more precisely, we exhale all permissions with exact checking later).

+  def Exhale(p: Expression, em: Boogie.Expr, eh: Boogie.Expr, error: ErrorMessage, check: Boolean, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = {

+    Exhale(p, em, eh, error, check, currentK, exactchecking, false) :::

+    Exhale(p, em, eh, error, check, currentK, exactchecking, true)

+  }

+  

+  def Exhale(p: Expression, em: Boogie.Expr, eh: Boogie.Expr, error: ErrorMessage, check: Boolean, currentK: Expr, exactchecking: Boolean, onlyExactCheckingPermissions: Boolean): List[Boogie.Stmt] = desugar(p) match {

     case pred@MemberAccess(e, p) if pred.isPredicate =>

       val tmp = Access(pred, Full);

       tmp.pos = pred.pos;

-      Exhale(tmp, em , eh, error, check, currentK, exactchecking)

+      Exhale(tmp, em , eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions)

     case AccessAll(obj, perm) => throw new InternalErrorException("should be desugared")

     case AccessSeq(s, None, perm) => throw new InternalErrorException("should be desugared")

     case acc@Access(e,perm) =>

-      val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;

-      val (starKV, starK) = NewBVar("starK", tint, true);

-

-      // check definedness

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

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

-      // if the mask does not contain sufficient permissions, try folding acc(e, fraction)

-      // TODO: include automagic again

-      // check that the necessary permissions are there and remove them from the mask

-      ExhalePermission(perm, Tr(e.e), memberName, currentK, acc.pos, error, em, exactchecking) :::

-      bassume(IsGoodMask(Mask)) ::

-      bassume(wf(Heap, Mask)) ::

-      bassume(wf(Heap, em))

+      val ec = needExactChecking(perm, exactchecking)

+      if (ec != onlyExactCheckingPermissions) Nil else {

+        val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;

+        val (starKV, starK) = NewBVar("starK", tint, true);

+        

+        // check definedness

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

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

+        // if the mask does not contain sufficient permissions, try folding acc(e, fraction)

+        // TODO: include automagic again

+        // check that the necessary permissions are there and remove them from the mask

+        ExhalePermission(perm, Tr(e.e), memberName, currentK, acc.pos, error, em, ec) :::

+        bassume(IsGoodMask(Mask)) ::

+        bassume(wf(Heap, Mask)) ::

+        bassume(wf(Heap, em))

+      }

     case acc @ AccessSeq(s, Some(member), perm) =>

       if (member.isPredicate) throw new NotSupportedException("not yet implemented");

-      val e = Tr(s);

-      val memberName = member.f.FullName;

-      

-      val (r, stmts) = extractKFromPermission(perm, currentK)

-      val n = extractEpsilonsFromPermission(perm);

       val ec = needExactChecking(perm, exactchecking);

-

-      stmts :::

-      (if (check) isDefined(s)(true) ::: isDefined(perm)(true) else Nil) :::

-      {

-        val (aV,a) = Boogie.NewTVar("alpha");

-        val (refV, ref) = Boogie.NewBVar("ref", tref, true);

-        val (fV, f) = Boogie.NewBVar("f", FieldType(a), true);

-        val (pcV,pc) = Boogie.NewBVar("p", tperm, true);

-        val mr = em(ref, memberName)("perm$R");

-        val mn = em(ref, memberName)("perm$N");

+      

+      if (ec != onlyExactCheckingPermissions) Nil else {

+        val e = Tr(s);

+        val memberName = member.f.FullName;

+        val (r, stmts) = extractKFromPermission(perm, currentK)

+        val n = extractEpsilonsFromPermission(perm);

         

-        // assert that the permission is positive

-        bassert((SeqContains(e, ref) ==>

-          (perm.permissionType match {

-            case PermissionType.Fraction => r > 0

-            case PermissionType.Mixed    => r > 0 || (r == 0 && n > 0)

-            case PermissionType.Epsilons => n > 0

-          })).forall(refV), error.pos, error.message + " The permission at " + acc.pos + " might not be positive.") ::

-        // make sure enough permission is available

-        bassert((SeqContains(e, ref) ==>

-          ((perm,perm.permissionType) match {

-            case _ if !ec     => mr > 0

-            case (Star,_)     => mr > 0

-            case (_,PermissionType.Fraction) => r <= mr && (r ==@ mr ==> 0 <= mn)

-            case (_,PermissionType.Mixed)    => r <= mr && (r ==@ mr ==> n <= mn)

-            case (_,PermissionType.Epsilons) => mr ==@ 0 ==> n <= mn

-          })).forall(refV), error.pos, error.message + " Insufficient permission at " + acc.pos + " for " + member.f.FullName) ::

-        // additional assumption on k if we have a star permission or use inexact checking

-        ( perm match {

-            case _ if !ec => bassume((SeqContains(e, ref) ==> (r < mr)).forall(refV)) :: Nil

-            case Star => bassume((SeqContains(e, ref) ==> (r < mr)).forall(refV)) :: Nil

-            case _ => Nil

-        }) :::

-        // update the map

-        (em := Lambda(List(aV), List(refV, fV),

-          (SeqContains(e, ref) && f ==@ memberName).thenElse(

-            Lambda(List(), List(pcV), (pc ==@ "perm$R").thenElse(mr - r, mn - n)),

-            em(ref, f))))

-      } :::

-      bassume(IsGoodMask(Mask)) ::

-      bassume(wf(Heap, Mask)) ::

-      bassume(wf(Heap, em))

-

-    case cr@Credit(ch, n) =>

+        stmts :::

+        (if (check) isDefined(s)(true) ::: isDefined(perm)(true) else Nil) :::

+        {

+          val (aV,a) = Boogie.NewTVar("alpha");

+          val (refV, ref) = Boogie.NewBVar("ref", tref, true);

+          val (fV, f) = Boogie.NewBVar("f", FieldType(a), true);

+          val (pcV,pc) = Boogie.NewBVar("p", tperm, true);

+          val mr = em(ref, memberName)("perm$R");

+          val mn = em(ref, memberName)("perm$N");

+          

+          // assert that the permission is positive

+          bassert((SeqContains(e, ref) ==>

+            (perm.permissionType match {

+              case PermissionType.Fraction => r > 0

+              case PermissionType.Mixed    => r > 0 || (r == 0 && n > 0)

+              case PermissionType.Epsilons => n > 0

+            })).forall(refV), error.pos, error.message + " The permission at " + acc.pos + " might not be positive.") ::

+          // make sure enough permission is available

+          bassert((SeqContains(e, ref) ==>

+            ((perm,perm.permissionType) match {

+              case _ if !ec     => mr > 0

+              case (Star,_)     => mr > 0

+              case (_,PermissionType.Fraction) => r <= mr && (r ==@ mr ==> 0 <= mn)

+              case (_,PermissionType.Mixed)    => r <= mr && (r ==@ mr ==> n <= mn)

+              case (_,PermissionType.Epsilons) => mr ==@ 0 ==> n <= mn

+            })).forall(refV), error.pos, error.message + " Insufficient permission at " + acc.pos + " for " + member.f.FullName) ::

+          // additional assumption on k if we have a star permission or use inexact checking

+          ( perm match {

+              case _ if !ec => bassume((SeqContains(e, ref) ==> (r < mr)).forall(refV)) :: Nil

+              case Star => bassume((SeqContains(e, ref) ==> (r < mr)).forall(refV)) :: Nil

+              case _ => Nil

+          }) :::

+          // update the map

+          (em := Lambda(List(aV), List(refV, fV),

+            (SeqContains(e, ref) && f ==@ memberName).thenElse(

+              Lambda(List(), List(pcV), (pc ==@ "perm$R").thenElse(mr - r, mn - n)),

+              em(ref, f))))

+        } :::

+        bassume(IsGoodMask(Mask)) ::

+        bassume(wf(Heap, Mask)) ::

+        bassume(wf(Heap, em))

+      }

+    case cr@Credit(ch, n) if !onlyExactCheckingPermissions =>

       val trCh = Tr(ch)

       (if (check)

          isDefined(ch)(true) :::

@@ -2025,14 +2042,14 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
          Nil) :::

       new Boogie.MapUpdate(Credits, trCh, new Boogie.MapSelect(Credits, trCh) - Tr(cr.N))

     case Implies(e0,e1) =>

-      (if(check) isDefined(e0)(true) else Nil) :::

-      Boogie.If(Tr(e0), Exhale(e1, em, eh, error, check, currentK, exactchecking), Nil)

+      (if(check && !onlyExactCheckingPermissions) isDefined(e0)(true) else Nil) :::

+      Boogie.If(Tr(e0), Exhale(e1, em, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions), Nil)

     case IfThenElse(con, then, els) =>

       (if(check) isDefined(con)(true) else Nil) :::

-      Boogie.If(Tr(con), Exhale(then, em, eh, error, check, currentK, exactchecking), Exhale(els, em, eh, error, check, currentK, exactchecking))

+      Boogie.If(Tr(con), Exhale(then, em, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions), Exhale(els, em, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions))

     case And(e0,e1) =>

-      Exhale(e0, em, eh, error, check, currentK, exactchecking) ::: Exhale(e1, em, eh, error, check, currentK, exactchecking)

-    case holds@Holds(e) => 

+      Exhale(e0, em, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions) ::: Exhale(e1, em, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions)

+    case holds@Holds(e) if !onlyExactCheckingPermissions => 

       (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(0 < new Boogie.MapSelect(Heap, Tr(e), "held"), error.pos, error.message + " The current thread might not hold lock at " + holds.pos + ".") ::

@@ -2040,7 +2057,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
       bassume(IsGoodMask(Mask)) ::

       bassume(wf(Heap, Mask)) ::

       bassume(wf(Heap, em))

-    case Eval(h, e) =>

+    case Eval(h, e) if !onlyExactCheckingPermissions =>

       val (evalHeap, evalMask, evalCredits, checks, proofOrAssume) = fromEvalState(h);

       val preGlobals = etran.FreshGlobals("eval")

       val preEtran = new ExpressionTranslator(List(Boogie.VarExpr(preGlobals(0).id), Boogie.VarExpr(preGlobals(1).id), Boogie.VarExpr(preGlobals(2).id)), currentClass);

@@ -2052,7 +2069,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
       bassume(wf(preEtran.Heap, preEtran.Mask)) ::

       bassert(proofOrAssume, p.pos, "Arguments for joinable might not match up.") ::

       preEtran.Exhale(List((e, error)), "eval", check, currentK, exactchecking)

-    case e => (if(check) isDefined(e)(true) else Nil) ::: List(bassert(Tr(e), error.pos, error.message + " The expression at " + e.pos + " might not evaluate to true."))

+    case e if !onlyExactCheckingPermissions => (if(check) isDefined(e)(true) else Nil) ::: List(bassert(Tr(e), error.pos, error.message + " The expression at " + e.pos + " might not evaluate to true."))

+    case _ => Nil

   }

   

   def extractKFromPermission(expr: Permission, currentK: Expr): (Expr, List[Boogie.Stmt]) = expr match {

diff --git a/Chalice/tests/permission-model/permission_arithmetic.chalice b/Chalice/tests/permission-model/permission_arithmetic.chalice
index 94cf30a3..fa457981 100644
--- a/Chalice/tests/permission-model/permission_arithmetic.chalice
+++ b/Chalice/tests/permission-model/permission_arithmetic.chalice
@@ -2,6 +2,8 @@ class Cell {
   var x: int;

   var i: int;

   var y: Cell;

+  var f: int;

+  var g: int;

   

   invariant rd(x);

   

@@ -189,5 +191,41 @@ class Cell {
     fold valid

   }

   

+  method a27()

+    requires acc(f,100-rd) && acc(f,rd)

+  {

+    assert acc(f) // ok, we have full access

+  }

+  

+  method a28()

+    requires acc(f)

+  {

+    call a27();

+    var x: int

+    x := f // ERROR: no permission left

+  }

+  

+  method a29()

+    requires acc(f, 100-rd) && acc(g, rd)

+  {  }

+

+  method a30()

+    requires acc(f, 100) && acc(g, rd)

+  {

+    call a29();

+    var tmp: int := this.g;

+  }

+  

+  method a31(c: Cell)

+    requires acc(f, 100-rd) && acc(c.f, rd)

+  {  }

+

+  method a32(c: Cell)

+    requires acc(f, 100) && acc(c.f, rd)

+  {

+    call a31(c);

+    var tmp: int := this.f;

+  }

+  

   method void() requires rd(x); ensures rd(x); {}

 }

diff --git a/Chalice/tests/permission-model/permission_arithmetic.output.txt b/Chalice/tests/permission-model/permission_arithmetic.output.txt
index 0b2b5335..f4859de5 100644
--- a/Chalice/tests/permission-model/permission_arithmetic.output.txt
+++ b/Chalice/tests/permission-model/permission_arithmetic.output.txt
@@ -1,13 +1,14 @@
 Verification of permission_arithmetic.chalice using parameters="" 

 

-  24.5: Assertion might not hold. The permission at 24.12 might not be positive.

-  40.5: The precondition at 33.14 might not hold. The permission at 33.14 might not be positive.

-  73.3: The postcondition at 75.13 might not hold. Insufficient fraction at 75.13 for Cell.x.

-  86.3: The postcondition at 88.13 might not hold. Insufficient epsilons at 88.22  for Cell.x.

-  103.20: Location might not be readable.

-  109.20: Location might not be readable.

-  145.5: Monitor invariant might not hold. Insufficient fraction at 6.13 for Cell.x.

-  162.3: The postcondition at 164.13 might not hold. The permission at 164.13 might not be positive.

-  174.3: The postcondition at 176.13 might not hold. Insufficient fraction at 176.13 for Cell.x.

+  26.5: Assertion might not hold. The permission at 26.12 might not be positive.

+  42.5: The precondition at 35.14 might not hold. The permission at 35.14 might not be positive.

+  75.3: The postcondition at 77.13 might not hold. Insufficient fraction at 77.13 for Cell.x.

+  88.3: The postcondition at 90.13 might not hold. Insufficient epsilons at 90.22  for Cell.x.

+  105.20: Location might not be readable.

+  111.20: Location might not be readable.

+  147.5: Monitor invariant might not hold. Insufficient fraction at 8.13 for Cell.x.

+  164.3: The postcondition at 166.13 might not hold. The permission at 166.13 might not be positive.

+  176.3: The postcondition at 178.13 might not hold. Insufficient fraction at 178.13 for Cell.x.

+  205.10: Location might not be readable.

 

-Boogie program verifier finished with 47 verified, 9 errors

+Boogie program verifier finished with 58 verified, 10 errors