Chalice: Check definedness of where-clause of channels (was missing before), and smoke test for 'false' where clauses. Due to the missing definedness check, a mistake in the specification of CopyLessMessagePassing-with-ack2.chalice was not detected (and has been fixed now).

5 files changed, 42 insertions, 16 deletions

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 4800b552..f2aae676 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -69,10 +69,10 @@ class Parser extends StandardTokenParsers {
             cl

         })

   def channelDecl =

-    "channel" ~> ident ~ formalParameters(true) ~ ("where" ~> expression ?) <~ Semi ^^ {

+    positioned("channel" ~> ident ~ formalParameters(true) ~ ("where" ~> expression ?) <~ Semi ^^ {

       case id ~ ins ~ None => Channel(id, ins, BoolLiteral(true))

       case id ~ ins ~ Some(e) => Channel(id, ins, e)

-    }

+    })

 

   /**

    * Member declarations

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index ccfdefe6..5580b3f3 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -23,8 +23,9 @@ 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)) :::

+        translateWhereClause(ch)

         /* TODO: waitlevel not allowed in postcondition of things forked (or, rather, joined) */

     }

   }

@@ -52,7 +53,7 @@ class Translator {
   /**********************************************************************

   *****************            MEMBERS                  *****************

   **********************************************************************/

-

+  

   def translateMember(member: Member): List[Decl] = {

     member match {

       case f: Field =>

@@ -73,6 +74,29 @@ class Translator {
         Nil

     }

   }

+  

+  def translateWhereClause(ch: Channel): List[Decl] = {

+    

+    // pick new k

+    val (whereKV, whereK) = Boogie.NewBVar("whereK", tint, true)

+    val whereKStmts = BLocal(whereKV) :: bassume(0 < whereK && 1000*whereK < permissionOnePercent)

+    

+    // check definedness of where clause

+    Proc(ch.channelId + "$whereClause$checkDefinedness",

+      NewBVarWhere("this", new Type(currentClass)) :: (ch.parameters map {i => Variable2BVarWhere(i)}),

+      Nil,

+      GlobalNames,

+      DefaultPrecondition(),

+      whereKStmts :::

+      DefinePreInitialState :::

+      InhaleWithChecking(List(ch.where), "channel where clause", whereK) :::

+      // smoke test: is the where clause equivalent to false?

+      (if (Chalice.smoke) {

+        val a = SmokeTest.initSmokeAssert(ch.pos, "Where clause of channel " + ch.channelId + " is equivalent to false.")

+        translateStatement(a.chaliceAssert, whereK)

+      } else Nil)

+    )

+  }

 

   def translateMonitorInvariant(invs: List[MonitorInvariant], pos: Position): List[Decl] = {

     val (h0V, h0) = NewBVar("h0", theap, true); val (m0V, m0) = NewBVar("m0", tmask, true);

@@ -148,6 +172,7 @@ class Translator {
       GlobalNames,

       DefaultPrecondition(),

       functionKStmts :::

+      //bassume(CanAssumeFunctionDefs) ::

       DefinePreInitialState :::

       // check definedness of the precondition

       InhaleWithChecking(Preconditions(f.spec) map { p => (if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition", functionK) :::

@@ -628,7 +653,7 @@ class Translator {
         // pick new k

         val (foldKV, foldK) = Boogie.NewBVar("foldK", tint, true)

         Comment("fold") ::

-        BLocal(foldKV) :: bassume(0 < foldK && 1000*foldK < permissionFull) ::

+        BLocal(foldKV) :: bassume(0 < foldK && 1000*foldK < percentPermission(1) && 1000*foldK < methodK) ::

         isDefined(e) :::

         isDefined(perm) :::

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

@@ -644,7 +669,7 @@ class Translator {
         // pick new k

         val (unfoldKV, unfoldK) = Boogie.NewBVar("unfoldK", tint, true)

         Comment("unfold") ::

-        BLocal(unfoldKV) :: bassume(0 < unfoldK && unfoldK < permissionFull) ::

+        BLocal(unfoldKV) :: bassume(0 < unfoldK && unfoldK < percentPermission(1) && 1000*unfoldK < methodK) ::

         isDefined(e) :::

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

         isDefined(perm) :::

@@ -667,7 +692,7 @@ class Translator {
         // pick new k for this fork

         val (asyncMethodCallKV, asyncMethodCallK) = Boogie.NewBVar("asyncMethodCallK", tint, true)

         BLocal(asyncMethodCallKV) ::

-        bassume(0 < asyncMethodCallK) :: // upper bounds are later provided by the exhale

+        bassume(0 < asyncMethodCallK && 1000*asyncMethodCallK < percentPermission(1) && 1000*asyncMethodCallK < methodK) ::

         Comment("call " + id) ::

         // declare the local variable, if needed

         { if (c.local == null)

@@ -971,7 +996,7 @@ class Translator {
     // pick new k for this method call

     val (methodCallKV, methodCallK) = Boogie.NewBVar("methodCallK", tint, true)

     BLocal(methodCallKV) ::

-    bassume(0 < methodCallK) :: // upper bounds are later provided by the exhale

+    bassume(0 < methodCallK && 1000*methodCallK < percentPermission(1) && 1000*methodCallK < methodK) ::

     Comment("call " + id) ::

     // introduce formal parameters and pre-state globals

     (for (v <- formalThisV :: formalInsV ::: formalOutsV) yield BLocal(Variable2BVarWhere(v))) :::

@@ -1024,7 +1049,7 @@ class Translator {
     Comment("while") ::

     // pick new k for this method call

     BLocal(whileKV) ::

-    bassume(0 < whileK) :: // upper bounds are later provided by the exhale

+    bassume(0 < whileK && 1000*whileK < percentPermission(1) && 1000*whileK < methodK) ::

     // save globals

     (for (v <- preLoopGlobals) yield BLocal(v)) :::

     (loopEtran.oldEtran.Heap := loopEtran.Heap) ::

@@ -1483,7 +1508,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         List(prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.")) :::

         // check precondition of the function by exhaling the precondition in tmpHeap/tmpMask/tmpCredits

         Comment("check precondition of call") ::

-        BLocal(funcappKV) :: bassume(0 < funcappK && 1000*funcappK < permissionFull) ::

+        BLocal(funcappKV) :: bassume(0 < funcappK && 1000*funcappK < percentPermission(1)) ::

         bassume(assumption) ::

         BLocal(tmpHeapV) :: (tmpHeap := Heap) ::

         BLocal(tmpMaskV) :: (tmpMask := Mask) :::

@@ -1507,7 +1532,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         val (unfoldingKV, unfoldingK) = Boogie.NewBVar("unfoldingK", tint, true)

         

         Comment("unfolding") ::

-        BLocal(unfoldingKV) :: bassume(0 < unfoldingK && 1000*unfoldingK < permissionFull) ::

+        BLocal(unfoldingKV) :: bassume(0 < unfoldingK && 1000*unfoldingK < percentPermission(1)) ::

         // check definedness

         receiverOk ::: isDefined(perm) :::

         // copy state into temporary variables

@@ -1907,7 +1932,6 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   

   def Exhale(predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = {

     if (predicates.size == 0) return Nil;

-    

     val (emV, em) = NewBVar("exhaleMask", tmask, true)

     Comment("begin exhale (" + occasion + ")") ::

     BLocal(emV) :: (em := Mask) ::

@@ -2103,7 +2127,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     case MethodEpsilon => (currentK, Nil)

     case ForkEpsilon(token) =>

       val fk = etran.Heap.select(Tr(token), forkK)

-      (fk, bassume(0 < fk && fk < permissionFull) /* this is always true for forkK */)

+      (fk, bassume(0 < fk && fk < percentPermission(1)) /* this is always true for forkK */)

     case Star =>

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

       (starK, BLocal(starKV) :: bassume(starK > 0 /* an upper bound is provided later by DecPermission */) :: Nil)

diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.chalice b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.chalice
index 77e0018d..3b03853d 100644
--- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.chalice
+++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.chalice
@@ -13,7 +13,7 @@ channel AckChannel(ch: C) where ch != null && credit(ch, -1); // ack
 

 channel C(msg: bool, n: Node, ackC: AckChannel) where 

   (!msg ==> acc(this.mu, 50) && acc(ackC.mu, 50)) &&

-  (msg ==> n != null && acc(n.next) && acc(n.mu) && credit(ackC, -1)); // cell 

+  (msg ==> n != null && acc(n.next) && acc(n.mu) && ackC != null && credit(ackC, -1)); // cell 

 

 class Node {

   var next: Node;

diff --git a/Chalice/tests/examples/SmokeTestTest.chalice b/Chalice/tests/examples/SmokeTestTest.chalice
index 44bba5da..6ff283ec 100644
--- a/Chalice/tests/examples/SmokeTestTest.chalice
+++ b/Chalice/tests/examples/SmokeTestTest.chalice
@@ -118,3 +118,4 @@ class Cell {
   }

 }

 

+channel C(msg: bool) where msg && !msg // SMOKE: contradiction
\ No newline at end of file
diff --git a/Chalice/tests/examples/SmokeTestTest.output.txt b/Chalice/tests/examples/SmokeTestTest.output.txt
index 697119cb..3d1cd786 100644
--- a/Chalice/tests/examples/SmokeTestTest.output.txt
+++ b/Chalice/tests/examples/SmokeTestTest.output.txt
@@ -18,5 +18,6 @@ The program did not fully verify; the smoke warnings might be misleading if cont
   100.5: Assumption introduces a contradiction.
   113.5: The statements after the method call statement are unreachable.
   116.3: Predicate Cell.valid is equivalent to false.
+  121.1: Where clause of channel C is equivalent to false.
 
-Boogie program verifier finished with 1 errors and 15 smoke test warnings.

+Boogie program verifier finished with 1 errors and 16 smoke test warnings.