Chalice: Allow _ as wildcard in the eval construct for parameters. Usage is demonstrated in a new test case.

5 files changed, 78 insertions, 10 deletions

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index f8824cee..1d74d636 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -370,6 +370,9 @@ class Parser extends StandardTokenParsers {
   def expressionList =

     repsep(expression, ",")

   def expression = positioned(iteExpr)

+  

+  def partialExpressionList =

+    repsep(expression | ("_" ^^^ VariableExpr("?")), ",")

 

   def iteExpr: Parser[Expression] =

         positioned(iffExpr ~ (("?" ~> iteExpr) ~ (":" ~> iteExpr) ?) ^^ {

@@ -442,7 +445,7 @@ class Parser extends StandardTokenParsers {
         case name ~ Some(es) => { e0: Expression => FunctionApplication(e0, name, es) } }

     | "." ~> "acquire" ~> exprBody ^^ { case eb => { e0: Expression => Eval(AcquireState(e0), eb) }}

     | "." ~> "release" ~> exprBody ^^ { case eb => { e0: Expression => Eval(ReleaseState(e0), eb) }}

-    | "." ~> "fork" ~> (callTarget ~ expressionList <~ ")") ~ exprBody ^^ {

+    | "." ~> "fork" ~> (callTarget ~ partialExpressionList <~ ")") ~ exprBody ^^ {

         case MemberAccess(obj,id) ~ args ~ eb => { e0: Expression => Eval(CallState(e0, obj, id, args), eb) }}

     )

   def exprBody =

@@ -583,7 +586,7 @@ class Parser extends StandardTokenParsers {
     (suffixExpr <~ ".") into { e =>

       ( "acquire" ^^^ AcquireState(e)

       | "release" ^^^ ReleaseState(e)

-      | "fork" ~> callTarget ~ expressionList <~ ")" ^^ {

+      | "fork" ~> callTarget ~ partialExpressionList <~ ")" ^^ {

           case MemberAccess(obj,id) ~ args => CallState(e, obj, id, args) }

       )}

 

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index efb19700..a8bdce62 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -1128,7 +1128,10 @@ object Resolver {
          if( ! token.typ.IsToken) context.Error(token.pos, "joinable is only applicable to tokens");

          ResolveExpr(obj, context, false, false)

          CheckNoGhost(obj, context)

-         args foreach { a => ResolveExpr(a, context, false, false); CheckNoGhost(a, context) }

+         args foreach { a => a match {

+            case VariableExpr("?") => 

+            case _ => ResolveExpr(a, context, false, false); CheckNoGhost(a, context)

+         }}

          // lookup method

          var typ: Class = IntClass

          obj.typ.LookupMember(id) match {

@@ -1141,8 +1144,12 @@ object Resolver {
                          " (" + args.length + " instead of " + m.ins.length + ")")

              else {

                for((actual, formal) <- args zip m.ins){

-                 if(! canAssign(formal.t.typ, actual.typ))

-                  context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")

+                 actual match {

+                    case VariableExpr("?") =>

+                    case _ => if (!canAssign(formal.t.typ, actual.typ))

+                        context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")

+                 }

+                 

              }

            }

          case _ => context.Error(obj.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index ea05d4bc..4243ead5 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -1746,10 +1746,10 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   }

 

   def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean, currentK: Expr): List[Boogie.Stmt] = desugar(p) match {

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

-      val chk = (if (check) {

-        isDefined(e)(true) ::: 

-        bassert(nonNull(Tr(e)), e.pos, "Receiver might be null.") :: Nil

+    case pred@MemberAccess(e, p) if pred.isPredicate => 
+      val chk = (if (check) {
+        isDefined(e)(true) ::: 
+        bassert(nonNull(Tr(e)), e.pos, "Receiver might be null.") :: Nil
       } else Nil)

       val tmp = Access(pred, Full);

       tmp.pos = pred.pos;

@@ -2119,6 +2119,14 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
       case CallState(token, obj, id, args) =>

         val argsSeq = CallArgs(Heap.select(Tr(token), "joinable"));

 

+        var f: ((Expression, Int)) => Expr =

+            (a: (Expression, Int)) => a match {

+                case (VariableExpr("?"),_) => true: Expr

+                case _ => new MapSelect(argsSeq, a._2) ==@ Tr(a._1)

+              }

+        var ll: List[(Expression, Int)] = null

+        ll = (args zip (1 until args.length+1).toList);

+        

         var i = 0;

         (CallHeap(Heap.select(Tr(token), "joinable")), 

          CallMask(Heap.select(Tr(token), "joinable")),

@@ -2129,7 +2137,9 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
          bassert(CanRead(Tr(token), "joinable"), obj.pos, "Joinable field of the token might not be readable.") ::

          bassert(Heap.select(Tr(token), "joinable") !=@ 0, obj.pos, "Token might not be active."),

          (new MapSelect(argsSeq, 0) ==@ Tr(obj) ) &&

-         (((args zip (1 until args.length+1).toList) map { a => new MapSelect(argsSeq, a._2) ==@ Tr(a._1)}).foldLeft(true: Expr){ (a: Expr, b: Expr) => a && b})

+         ((ll map { 

+            f

+         }).foldLeft(true: Expr){ (a: Expr, b: Expr) => a && b})

         )

     }

   }

diff --git a/Chalice/tests/examples/Solver.chalice b/Chalice/tests/examples/Solver.chalice
new file mode 100644
index 00000000..0de8a987
--- /dev/null
+++ b/Chalice/tests/examples/Solver.chalice
@@ -0,0 +1,44 @@
+class Client {

+  

+  method main(p: Problem, s: Solver) returns (r: int)

+    requires acc(p.f) && s != null

+    ensures acc(p.f)

+  {

+    // start randomized computations

+    var tk1: token<Solver.solve>

+    var tk2: token<Solver.solve>

+    call tk1 := s.start(p)

+    call tk2 := s.start(p)

+    

+    // get the results

+    var r1: int 

+    join r1 := tk1

+    var r2: int

+    join r2:= tk2

+    r := r1 > r2 ? r1 : r2

+  }

+  

+}

+class Solver {

+  

+  method solve(p: Problem, d: Data) returns (r: int)

+    requires rd(p.f)

+    requires acc(d.*)

+    ensures rd(p.f)

+  { /* ... */ }

+  

+  method start(p: Problem)

+    returns (tk: token<Solver.solve>)

+    requires rd(p.f)

+    ensures acc(p.f, rd-rd(tk))

+    ensures acc(tk.joinable) && tk.joinable;

+    ensures eval(tk.fork this.solve(p,_), true)

+  {

+    var d: Data := new Data

+    /* .. perform some set-up/initialization and prepare the data d for the solve method */

+    fork tk := solve(p, d)

+  }

+  

+}

+class Problem { var f: int }

+class Data { var f: int; var g: int }

diff --git a/Chalice/tests/examples/Solver.output.txt b/Chalice/tests/examples/Solver.output.txt
new file mode 100644
index 00000000..e88f63d9
--- /dev/null
+++ b/Chalice/tests/examples/Solver.output.txt
@@ -0,0 +1,4 @@
+Verification of Solver.chalice using parameters="" 

+

+

+Boogie program verifier finished with 10 verified, 0 errors