Quantified permissions parsed and translated incorrectly

[viper-admin]

Created by @vakaras on 2015-08-24 14:20

acc(cells[*].cell.val) is parsed as a field [*] access on cells.

More complete example:

#!Chalice

//:: UnexpectedOutput(typechecker.error, /Chalice2Silver/issue/72/)
class Cell {
  var val: int
}

class Cell2 {
  var cell: Cell
}

class Test {
  var cells: seq<Cell2>

  method test()
    requires acc(cells[*].cell)
    //:: UnexpectedOutput(typechecker.error, /Chalice2Silver/issue/72/)
    requires acc(cells[*].cell.val)
  {
  }
}

Reported error:

[info] The following output occurred during testing, but should not have according to the test annotations:
[info]   [typechecker.error] undeclared member val in class int (chalice2silver-72.chalice,14:18)
[info]   [typechecker.error] undeclared member cell in class int (chalice2silver-72.chalice,2:1)
[info]   [typechecker.error] undeclared member [*] in class seq<Cell2> (chalice2silver-72.chalice,2:1) (AnnotationBasedTestSuite.scala:59)

Parser can be fixed with this change:

#!diff
diff -r <https://github.com/viperproject/chalice2silver/commit/a1a1dee633c51b985b50435b9fb05cf597092eb9> src/main/scala/chalice/Parser.scala
--- a/src/main/scala/chalice/Parser.scala       Mon Aug 24 16:06:29 2015 +0200
+++ b/src/main/scala/chalice/Parser.scala       Mon Aug 24 16:06:50 2015 +0200
@@ -582,9 +582,25 @@
       ) ^^ {
         case MemberAccess(obj, "*") ~ p => AccessAll(obj, p);
         case MemberAccess(obj, "[*].*") ~ p => AccessSeq(obj, None, p);
-        case MemberAccess(MemberAccess(obj, "[*]"), f) ~ p => AccessSeq(obj, Some(MemberAccess(At(obj, IntLiteral(0)), f)), p);
         case (b @ BackPointerMemberAccess(_,_,_)) ~ p => BackPointerAccess(b, p);
-        case (m @ MemberAccess(_,_)) ~ p => Access(m, p)
+        case (m @ MemberAccess(_,_)) ~ p =>
+          def convert(m: MemberAccess): Option[(Expression, MemberAccess)] = m match {
+            case MemberAccess(MemberAccess(obj, "[*]"), f) =>
+              Some(obj, MemberAccess(At(obj, IntLiteral(0)), f))
+            case MemberAccess(m@MemberAccess(_, _), f) =>
+              convert(m) match {
+                case Some((obj, memberAccess)) => Some(obj, MemberAccess(memberAccess, f))
+                case None => None
+              }
+            case _ => None
+          }
+          val acccessPredicate = convert(m) match {
+            case Some((obj, memberAccess)) =>
+              AccessSeq(obj, Some(memberAccess), p)
+            case None =>
+              Access(m, p)
+          }
+          acccessPredicate
       })
     | "credit" ~> "(" ~> expression ~ ("," ~> expression ?) <~ ")" ^^ {
         case ch ~ n => Credit(ch, n) }

However, fixing translation is more involved.