Merge pull request #572 from viperproject/perm_multiplication

Added support for perm-perm-multiplication

Author: marcoeilers

src/main/scala/viper/silver/ast/Expression.scala

@@ -330,6 +330,13 @@ case class PermDiv(left: Exp, right: Exp)(val pos: Position = NoPosition, val in
     (if(left.typ != Perm) Seq(ConsistencyError(s"First parameter of permission division expression must be Perm, but found ${left.typ}", left.pos)) else Seq()) ++
     (if(right.typ != Int) Seq(ConsistencyError(s"Second parameter of permission division expression must be Int, but found ${right.typ}", right.pos)) else Seq())
 }
+
+case class PermPermDiv(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(PermDivOp) with PermExp with ForbiddenInTrigger
+{
+  override lazy val check : Seq[ConsistencyError] =
+    (if(left.typ != Perm) Seq(ConsistencyError(s"First parameter of permission division expression must be Perm, but found ${left.typ}", left.pos)) else Seq()) ++
+      (if(right.typ != Perm) Seq(ConsistencyError(s"Second parameter of permission-permission division expression must be Perm, but found ${right.typ}", right.pos)) else Seq())
+}
 /** The permission currently held for a given resource. */
 case class CurrentPerm(res: ResourceAccess)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends PermExp
 

src/main/scala/viper/silver/parser/ParseAst.scala

@@ -549,6 +549,7 @@ class PBinExp(val left: PExp, val opName: String, val right: PExp)(val pos: (Pos
     case "/" => List(
       Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Perm),
       Map(POpApp.pArgS(0) -> Perm, POpApp.pArgS(1) -> Int, POpApp.pResS -> Perm),
+      Map(POpApp.pArgS(0) -> Perm, POpApp.pArgS(1) -> Perm, POpApp.pResS -> Perm),
       Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Int)
     )
     case "\\" | "%" => List(

src/main/scala/viper/silver/parser/Translator.scala

@@ -290,9 +290,11 @@ case class Translator(program: PProgram) {
               case _ => sys.error("should not occur in type-checked program")
             }
           case "/" =>
-            assert(r.typ==Int)
             l.typ match {
-              case Perm => PermDiv(l, r)(pos)
+              case Perm => r.typ match {
+                case Int => PermDiv(l, r)(pos)
+                case Perm => PermPermDiv(l, r)(pos)
+              }
               case Int  =>
                 assert (r.typ==Int)
                 if (ttyp(pbe.typ) == Int)

src/test/resources/all/basic/arithmetic.vpr

@@ -45,3 +45,17 @@ method t6() {
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert 2/3 == 3/4 // / is interpreted as Perm-typed division
 }
+
+method t6(p: Perm)
+{
+    var r1 : Perm
+    var r2: Perm
+    var one: Perm
+    one := 1/1
+    r1 := p * one
+    r2 := p * (2/1)
+    assert r1 == p
+    assert r2 - r1 == p
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert r2 == p
+}