Implicitly declare as local variables undeclared variables occurring as LHS's of CALL and RECEIVE statements (as was already done for FORK statements).

10 files changed, 182 insertions, 82 deletions

diff --git a/Chalice/examples/Answer b/Chalice/examples/Answer
index e40b7287..438a9dd6 100644
--- a/Chalice/examples/Answer
+++ b/Chalice/examples/Answer
@@ -1,7 +1,4 @@
 start 

------- Running regression test AssociationList.chalice 

-

-Boogie program verifier finished with 12 verified, 0 errors

 ------ Running regression test cell.chalice 

   142.5: Assertion might not hold. Insufficient fraction at 142.12 for Cell.valid.

 

@@ -152,9 +149,6 @@ The program did not typecheck.
 31.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)

 32.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)

 33.19: undeclared member o in class C

-33.10: undefined local variable a

-33.12: undefined local variable b

-33.14: undefined local variable c

 33.5: call of undeclared member m in class int

 34.5: wrong number of actual in-parameters in call to C.m (1 instead of 0)

 34.5: wrong number of actual out-parameters in call to C.m (1 instead of 0)

@@ -163,8 +157,24 @@ The program did not typecheck.
 58.17: undeclared member sqrt2 in class C

 58.25: undeclared member sqrt2 in class C

 62.17: undeclared member s in class C

-62.10: undefined local variable v

 62.5: call of undeclared member M in class int

+82.5: call of undeclared member MyMethodX in class ImplicitC

+83.12: undefined local variable a

+83.16: undefined local variable b

+83.16: undeclared member k in class int

+88.13: the type of the formal argument is not assignable to the actual parameter (expected: ImplicitC, found: int)

+88.13: duplicate actual out-parameter: a

+89.16: undeclared member b in class ImplicitC

+89.16: undeclared member k in class int

+96.21: undeclared member chX in class ImplicitC

+96.5: receive expression (which has type int) does not denote a channel

+97.12: undefined local variable a

+97.16: undefined local variable b

+97.16: undeclared member k in class int

+104.16: the type of the formal argument is not assignable to the actual parameter (expected: ImplicitC, found: int)

+104.16: duplicate actual out-parameter: a

+105.16: undeclared member b in class ImplicitC

+105.16: undeclared member k in class int

 ------ Running regression test prog1.chalice 

   9.10: Location might not be readable.

   25.5: Location might not be writable

@@ -195,6 +205,9 @@ Boogie program verifier finished with 51 verified, 4 errors
   27.7: The held field of the target of the release statement might not be writable.

 

 Boogie program verifier finished with 6 verified, 3 errors

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

+

+Boogie program verifier finished with 8 verified, 0 errors

 ------ Running regression test RockBand.chalice 

   27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.

   41.10: Location might not be readable.

@@ -207,12 +220,6 @@ Boogie program verifier finished with 29 verified, 6 errors
 ------ Running regression test swap.chalice 

 

 Boogie program verifier finished with 5 verified, 0 errors

------- Running regression test GhostConst.chalice 

-The program did not typecheck.

-7.27: undeclared member c in class C

-13.10: ghost variable not allowed here

-21.10: ghost variable not allowed here

-29.10: ghost fields not allowed here

 ------ Running regression test OwickiGries.chalice 

 

 Boogie program verifier finished with 5 verified, 0 errors

@@ -232,11 +239,3 @@ Boogie program verifier finished with 29 verified, 3 errors
 ------ Running regression test RockBand-automagic.chalice 

 

 Boogie program verifier finished with 35 verified, 0 errors

------- Running regression test Leaks.chalice 

-  6.3: Monitor invariant is not allowed to hold write permission to this.mu

-  11.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu

-  16.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu

-  29.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu

-  62.3: Monitor invariant is not allowed to hold write permission to this.mu

-

-Boogie program verifier finished with 7 verified, 5 errors

diff --git a/Chalice/examples/ImplicitLocals.chalice b/Chalice/examples/ImplicitLocals.chalice
new file mode 100644
index 00000000..15ebe8e0
--- /dev/null
+++ b/Chalice/examples/ImplicitLocals.chalice
@@ -0,0 +1,27 @@
+class C {

+  var k: int;

+

+  method MyMethod() returns (x: int, y: C)

+    requires acc(k)

+    ensures acc(y.k) && x < y.k

+  {

+    x := k - 15;

+    y := this;

+  }

+

+  method B() {

+    var c := new C;

+    call a, b := c.MyMethod();

+    assert a < b.k;

+  }

+

+  method D() {

+    var ch := new Ch;

+    var c := new C;

+    send ch(c.k - 15, c);  // give ourselves some credit

+    receive a, b := ch;

+    assert a < b.k;

+  }

+}

+

+channel Ch(x: int, y: C) where acc(y.k) && x < y.k;

diff --git a/Chalice/examples/prog0.chalice b/Chalice/examples/prog0.chalice
index da351c85..7bcb1505 100644
--- a/Chalice/examples/prog0.chalice
+++ b/Chalice/examples/prog0.chalice
@@ -63,3 +63,47 @@ class C {
   }

 }

 class D { }

+

+// ----- tests specifically of implicit locals in CALL and RECEIVE statements

+

+class ImplicitC {

+  var k: int;

+

+  method MyMethod() returns (x: int, y: ImplicitC)

+    requires acc(k)

+    ensures acc(y.k) && x < y.k

+  {

+    x := k - 15;

+    y := this;

+  }

+

+  method B0() {

+    var c := new ImplicitC;

+    call a, b := c.MyMethodX();  // error: method not found (so what is done with a,b?)

+    assert a < b.k;

+  }

+

+  method B1() {

+    var c := new ImplicitC;

+    call a, a := c.MyMethod();  // error: a occurs twice

+    assert a < b.k;

+  }

+

+  method D0() {

+    var ch := new Ch;

+    var c := new ImplicitC;

+    send ch(c.k - 15, c);  // give ourselves some credit

+    receive a, b := chX;  // error: channel not found (so what is done with a,b?)

+    assert a < b.k;

+  }

+

+  method D1() {

+    var ch := new Ch;

+    var c := new ImplicitC;

+    send ch(c.k - 15, c);  // give ourselves some credit

+    receive a, a := ch;  // error: a occurs twice

+    assert a < b.k;

+  }

+}

+

+channel Ch(x: int, y: ImplicitC) where acc(y.k) && x < y.k;

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 7ad95899..61d7a0f3 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -189,7 +189,8 @@ case class LocalVar(id: String, t: Type, const: boolean, ghost: boolean, rhs: Op
     else

       new Variable(id, t){override val IsGhost = ghost}

 }

-case class Call(lhs: List[VariableExpr], obj: Expression, id: String, args: List[Expression]) extends Statement {

+case class Call(declaresLocal: List[boolean], lhs: List[VariableExpr], obj: Expression, id: String, args: List[Expression]) extends Statement {

+  var locals = List[Variable]()

   var m: Method = null

 }

 case class Install(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement

@@ -217,7 +218,8 @@ case class Signal(obj: Expression, id: String, all: boolean) extends Statement {
 }

 case class Send(ch: Expression, args: List[Expression]) extends Statement {

 }

-case class Receive(ch: Expression, outs: List[VariableExpr]) extends Statement {

+case class Receive(declaresLocal: List[boolean], ch: Expression, outs: List[VariableExpr]) extends Statement {

+  var locals = List[Variable]()

 }

 case class Fold(pred: PermissionExpr) extends Statement

 case class Unfold(pred: PermissionExpr) extends Statement

@@ -241,6 +243,7 @@ case class LockBottomLiteral extends Literal
 case class VariableExpr(id: String) extends Expression {

   var v: Variable = null

   def this(vr: Variable) = { this(vr.id); v = vr; typ = vr.t.typ }

+  def Resolve(vr: Variable) = { v = vr; typ = vr.t.typ }

 }

 case class Result extends Expression

 sealed abstract class ThisExpr extends Expression {

diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala
index 18c1f849..110f7a2a 100644
--- a/Chalice/src/ChaliceToCSharp.scala
+++ b/Chalice/src/ChaliceToCSharp.scala
@@ -94,7 +94,7 @@ class ChaliceToCSharp {
       case Predicate(_, _) => indent + "//predicate" + nl

     }

   }

-  

+

   def convertStatement(statement: Statement): String = {

     statement match {

       case Assert(e) => indent + "// assert" + nl

@@ -112,7 +112,8 @@ class ChaliceToCSharp {
         indent + x + " = " + convertExpression(rhs) + ";" + nl

       case WhileStmt(guard, _, _, body) =>

         indent + "while (" + convertExpression(guard) + ")" + nl + convertStatement(body) + nl

-      case Call(lhs, target, id, args) =>

+      case c@Call(_, lhs, target, id, args) =>

+        declareLocals(c.locals) +

         indent + convertExpression(target) + "." + id + "(" + 

           repsep(args map convertExpression, ", ") + 

           (if(args.length > 0 && lhs.length > 0) ", " else "") +

@@ -148,11 +149,19 @@ class ChaliceToCSharp {
         (if(lhs.length > 0) ", " else "") + convertExpression(token) + "." + "async" + ");" + nl

       case s@Send(ch, args) =>

         indent + convertExpression(ch) + ".Send(" + repsep(args map convertExpression, ", ") + ")" + ";" + nl

-      case r@Receive(ch, outs) =>

+      case r@Receive(_, ch, outs) =>

+        declareLocals(r.locals) +

         indent + convertExpression(ch) + ".Receive(" + repsep(outs map { out => "out " + convertExpression(out)}, ", ") + ")" + ";" + nl

     }

   }

   

+  def declareLocals(locals: List[Variable]) = {

+    var s = ""

+    for (v <- locals)

+      s = s + indent + convertType(v.t) + " " + v.id + ";" + nl

+    s

+  }

+

   def convertExpression(expression: RValue): String = {

     expression match {

       case IntLiteral(n) => "" + n

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index f9d21f76..a92e5b40 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -207,7 +207,9 @@ class Parser extends StandardTokenParsers {
         case fa@FunctionApplication(ImplicitThisExpr(), name, args) => Semi ^^^ {val va = VariableExpr(name); va.pos = fa.pos; Send(va, args)}

         case e => "(" ~> expressionList <~ ")" <~ Semi ^^ { case args => Send(e, args) }}})

     | "receive" ~> (identList <~ ":=" ?) ~ expression <~ Semi ^^ {

-        case outs ~ e => Receive(e, ExtractList(outs)) }

+        case outs ~ e =>

+          val lhs = ExtractList(outs)

+          Receive(declareImplicitLocals(lhs), e, lhs) }

     )

   def localVarStmt(const: boolean, ghost: boolean) =

       idTypeOpt ~ (":=" ~> Rhs ?) <~ Semi ^^ {

@@ -245,10 +247,22 @@ class Parser extends StandardTokenParsers {
     ( "invariant" ~> expression <~ Semi ^^ { case e => (e,Nil) }

     | "lockchange" ~> expressionList <~ Semi ^^ { case ee => (null,ee) }

     )

+  def declareImplicitLocals(lhs: List[VariableExpr]) =

+    for (v <- lhs) yield

+      if (currentLocalVariables contains v.id)

+        false

+      else {

+        currentLocalVariables = currentLocalVariables + v.id

+        true

+      }

   def callStmt =

     callSignature ^? ({

-      case outs ~ VariableExpr(id) ~ args => Call(ExtractList(outs), new ImplicitThisExpr, id, args)

-      case outs ~ MemberAccess(obj,id) ~ args => Call(ExtractList(outs), obj, id, args)

+      case outs ~ VariableExpr(id) ~ args =>

+        val lhs = ExtractList(outs)

+        Call(declareImplicitLocals(lhs), lhs, new ImplicitThisExpr, id, args)

+      case outs ~ MemberAccess(obj,id) ~ args =>

+        val lhs = ExtractList(outs)

+        Call(declareImplicitLocals(lhs), lhs, obj, id, args)

     }, t => "bad call statement")

   def callSignature =

     (identList <~ ":=" ?) ~ callTarget ~ expressionList <~ ")" <~ Semi

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index fb94f711..a97a04f9 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -90,7 +90,7 @@ object PrintProgram {
       print(id + ": " + t.id)

       rhs match { case None => case Some(rhs) => print(" := "); Rhs(rhs) }

       println(Semi)

-    case Call(outs, obj, id, args) =>

+    case Call(_, outs, obj, id, args) =>

       print("call ")

       outs match {

         case Nil =>

@@ -150,7 +150,7 @@ object PrintProgram {
       println(Semi)

     case Send(ch, args) =>

       print("send "); Expr(ch); print("("); ExprList(args); print(")"); println(Semi)

-    case Receive(ch, outs) =>

+    case Receive(_, ch, outs) =>

       print("receive ")

       outs match {

         case Nil =>

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index f592740d..00daaa92 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -233,14 +233,17 @@ object Resolver {
               ResolveExpr(lhs, ctx, false, false)(false)

               ResolveAssign(lhs, rhs, oldCtx)

           }

-        case c@CallAsync(declaresLocal, token, obj, id, args) =>

+        case c: CallAsync =>

           ResolveStmt(c, ctx)

-          if (declaresLocal) {

-            c.local = new Variable(token.id, TokenType(new Type(obj.typ), id))

-            ResolveType(c.local.t, ctx)

+          if (c.local != null) {

             ctx = ctx.AddVariable(c.local)

-            ResolveExpr(token, ctx, false, false)(false)

           }

+        case c: Call =>

+          ResolveStmt(c, ctx)

+          for (v <- c.locals) { ctx = ctx.AddVariable(v) } 

+        case r: Receive =>

+          ResolveStmt(r, ctx)

+          for (v <- r.locals) { ctx = ctx.AddVariable(v) } 

         case s =>

           ResolveStmt(s, ctx)

       }

@@ -281,22 +284,10 @@ object Resolver {
       if (! lhs.isPredicate && !canAssign(lhs.typ, rhs.typ)) context.Error(fu.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)

       if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(rhs, context)

     case lv:LocalVar => throw new Exception("unexpected LocalVar; should have been handled in BlockStmt above")

-    case c @ Call(lhs, obj, id, args) =>

+    case c @ Call(declaresLocal, lhs, obj, id, args) =>

       ResolveExpr(obj, context, false, false)(false)

       CheckNoGhost(obj, context)

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

-      var vars = Set[Variable]()

-      for (v <- lhs) {

-        ResolveExpr(v, context, false, false)(false)

-        if (v.v != null) {

-          if (v.v.IsImmutable) context.Error(v.pos, "cannot use immutable variable " + v.id + " as actual out-parameter")

-          if (vars contains v.v) {

-            context.Error(v.pos, "duplicate actual out-parameter: " + v.id)

-          } else {

-            vars = vars + v.v

-          }

-        }

-      }

       // lookup method

       var typ: Class = IntClass

       obj.typ.LookupMember(id) match {

@@ -316,13 +307,8 @@ object Resolver {
           if (lhs.length != m.outs.length)

             context.Error(c.pos, "wrong number of actual out-parameters in call to " + obj.typ.FullName + "." + id +

                           " (" + lhs.length + " instead of " + m.outs.length + ")")

-          else {

-            for((out, l) <- m.outs zip lhs){

-              if(! canAssign(l.typ, out.t.typ))

-                context.Error(l.pos, "the out parameter cannot be assigned to the lhs (expected: " + l.typ.FullName + ", found: " + out.t.FullName + ")")

-            }

-          }

-

+          else

+            c.locals = ResolveLHS(declaresLocal, lhs, m.outs, context)

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

       }

     case Install(obj, lowerBounds, upperBounds) =>

@@ -408,7 +394,9 @@ object Resolver {
       }

       // resolve the token

       if (declaresLocal) {

-        // this is taken care of in the caller that handles the enclosing block statement

+        c.local = new Variable(token.id, TokenType(new Type(obj.typ), id))

+        ResolveType(c.local.t, context)

+        token.Resolve(c.local)

       } else if (token != null) {

         ResolveExpr(token, context, false, false)(false)

         if(! canAssign(token.typ, TokenClass(new Type(obj.typ), id)))

@@ -488,39 +476,51 @@ object Resolver {
           }

         case _ => context.Error(s.pos, "send expression (which has type " + ch.typ.FullName + ") does not denote a channel")

       }

-    case r@Receive(ch, outs) =>

+    case r@Receive(declaresLocal, ch, outs) =>

       ResolveExpr(ch, context, false, false)(false)

       CheckNoGhost(ch, context)

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

-      // check the outs to be appropriate actually out parameters

-      var vars = Set[Variable]()

-      for (v <- outs) {

-        ResolveExpr(v, context, false, false)(false)

-        if (v.v != null) {

-          if (v.v.IsImmutable) context.Error(v.pos, "cannot use immutable variable " + v.id + " as actual out-parameter of receive")

-          if (vars contains v.v) {

-            context.Error(v.pos, "duplicate actual out-parameter: " + v.id)

-          } else {

-            vars = vars + v.v

-          }

-        }

-      }

       // match types of arguments

       ch.typ match {

         case ChannelClass(channel) =>

           if (outs.length != channel.parameters.length)

             context.Error(r.pos, "wrong number of actual out-parameters in receive for channel type " + ch.typ.FullName +

                           " (" + outs.length + " instead of " + channel.parameters.length + ")")

-          else {

-            for ((actual, formal) <- outs zip channel.parameters) {

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

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

-            }

-          }

+          else

+            r.locals = ResolveLHS(declaresLocal, outs, channel.parameters, context)

         case _ => context.Error(r.pos, "receive expression (which has type " + ch.typ.FullName + ") does not denote a channel")

       }

   }

 

+  def ResolveLHS(declaresLocal: List[boolean], actuals: List[VariableExpr], formals: List[Variable], context: ProgramContext): List[Variable] = {

+    var locals = List[Variable]()

+    var vars = Set[Variable]()

+    var ctx = context

+    for (((declareLocal, actual), formal) <- declaresLocal zip actuals zip formals) {

+      if (declareLocal) {

+        val local = new Variable(actual.id, new Type(formal.t.typ))

+        locals = locals + local

+        ResolveType(local.t, ctx)

+        actual.Resolve(local)

+        vars = vars + actual.v

+        ctx = ctx.AddVariable(local)

+      } else {

+        ResolveExpr(actual, ctx, false, false)(false)

+        CheckNoGhost(actual, ctx)

+        if (actual.v != null) {

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

+            ctx.Error(actual.pos, "the type of the formal argument is not assignable to the actual parameter (expected: " +

+                          formal.t.FullName + ", found: " + actual.typ.FullName + ")")

+          if (vars contains actual.v)

+            ctx.Error(actual.pos, "duplicate actual out-parameter: " + actual.id)

+          else if (actual.v.IsImmutable)

+            ctx.Error(actual.pos, "cannot use immutable variable " + actual.id + " as actual out-parameter")

+          vars = vars + actual.v

+        }

+      }

+    }

+    locals

+  }

+

   def ResolveBounds(lowerBounds: List[Expression], upperBounds: List[Expression], context: ProgramContext, descript: String) =

     for (b <- lowerBounds ++ upperBounds) {

       ResolveExpr(b, context, true, false)(false)

@@ -541,7 +541,7 @@ object Resolver {
       if (lhs.v != null) Set(lhs.v) else Set()  // don't assume resolution was successful

     case lv: LocalVar =>

       lv.rhs match { case None => Set() case Some(_) => Set(lv.v) }

-    case Call(lhs, obj, id, args) =>

+    case Call(_, lhs, obj, id, args) =>

       (lhs :\ Set[Variable]()) { (ve,vars) => if (ve.v != null) vars + ve.v else vars }

     case _ => Set()

   }

@@ -614,7 +614,7 @@ object Resolver {
     case ve @ VariableExpr(id) =>

       context.LookupVariable(id) match {

         case None => context.Error(ve.pos, "undefined local variable " + id); ve.typ = IntClass

-        case Some(v) => ve.v = v; ve.typ = v.t.typ }

+        case Some(v) => ve.Resolve(v) }

     case v:ThisExpr => v.typ = context.CurrentClass

     case sel @ MemberAccess(e, id) =>

       ResolveExpr(e, context, twoStateContext, false)

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 46805d59..b89fd91a 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -656,7 +656,7 @@ class Translator {
           (SubstThisAndVars(channel.where, formalThis, channel.parameters, formalParams),

            ErrorMessage(s.pos, "The where clause at " + channel.where.pos + " might not hold."))),

           "channel where clause")

-      case r@Receive(ch, outs) =>

+      case r@Receive(_, ch, outs) =>

         val channel = ch.typ.asInstanceOf[ChannelClass].ch

         val formalThisV = new Variable("this", new Type(ch.typ))

         val formalThis = new VariableExpr(formalThisV)

@@ -678,6 +678,8 @@ class Translator {
         (for (v <- formalParams) yield Havoc(v)) :::

         // inhale where clause

         Inhale(List(SubstThisAndVars(channel.where, formalThis, channel.parameters, formalParams)), "channel where clause") :::

+        // declare any new local variables among the actual outs

+        (for (v <- r.locals) yield BLocal(Variable2BVarWhere(v))) :::

         // assign formal outs to actual outs

         (for ((v,e) <- outs zip formalParams) yield (v := e)) :::

         // decrease credits

@@ -822,6 +824,8 @@ class Translator {
     // inhale postconditions (using the state before the call as the "old" state)

     postEtran.Inhale(Postconditions(c.m.spec) map

                      (p => SubstThisAndVars(p, formalThis, c.m.ins ++ c.m.outs, formalIns ++ formalOuts)) , "postcondition", false) :::

+    // declare any new local variables among the actual outs

+    (for (v <- c.locals) yield BLocal(Variable2BVarWhere(v))) :::

     // assign formal outs to actual outs

     (for ((v,e) <- lhs zip formalOuts) yield (v :=e))

   }

diff --git a/Chalice/test.bat b/Chalice/test.bat
index fde3cc60..42124855 100644
--- a/Chalice/test.bat
+++ b/Chalice/test.bat
@@ -9,7 +9,7 @@ REM to do: Leaks -checkLeaks
 

 for %%f in (cell counter dining-philosophers ForkJoin HandOverHand

             iterator iterator2 producer-consumer

-            prog0 prog1 prog2 prog3 prog4

+            prog0 prog1 prog2 prog3 prog4 ImplicitLocals

             RockBand swap OwickiGries ProdConsChannel) do (

   echo   Testing %%f.chalice ...

   echo ------ Running regression test %%f.chalice >> Output