Giving Perm-typed expressions higher priority so that Perm is always the default for anything ambiguous (#855)

Author: marcoeilers

Diff for: src/main/scala/viper/silver/parser/ParseAstKeyword.scala

@@ -345,16 +345,16 @@ trait PUnaryOp extends POperator with PSignaturesOp
 trait PBinaryOp extends POperator with PSignaturesOp with LeftSpace with RightSpace
 trait PArithOp extends PBinaryOp {
   override def signatures = List(
-    Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Int),
-    Map(POpApp.pArgS(0) -> Perm, POpApp.pArgS(1) -> Perm, 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))
 }
 trait PIntOp extends PBinaryOp {
   override def signatures = List(Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Int))
 }
 trait PCmpOp extends PBinaryOp {
   override def signatures = List(
-    Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Bool),
-    Map(POpApp.pArgS(0) -> Perm, POpApp.pArgS(1) -> Perm, POpApp.pResS -> Bool))
+    Map(POpApp.pArgS(0) -> Perm, POpApp.pArgS(1) -> Perm, POpApp.pResS -> Bool),
+    Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Bool))
 }
 trait PLogicalOp extends PBinaryOp {
   override def signatures = List(Map(POpApp.pArgS(0) -> Bool, POpApp.pArgS(1) -> Bool, POpApp.pResS -> Bool))
@@ -409,11 +409,10 @@ object PSymOp {
   }
   case object Div     extends PSym("/")   with PSymbolOp with PBinaryOp {
     override def signatures = List(
-      // The following two are not necessary if `Int` is a subtype of `Perm`
-      Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Perm),
+      Map(POpApp.pArgS(0) -> Perm, POpApp.pArgS(1) -> Perm, POpApp.pResS -> Perm),
       Map(POpApp.pArgS(0) -> Perm, POpApp.pArgS(1) -> Int, POpApp.pResS -> Perm),
+      Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Perm),
       Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Int),
-      Map(POpApp.pArgS(0) -> Perm, POpApp.pArgS(1) -> Perm, POpApp.pResS -> Perm),
     )
   }
   case object ArithDiv extends PSym("\\") with PSymbolOp with PBinaryOp with PIntOp
@@ -428,8 +427,8 @@ object PSymOp {
 
   case object Neg     extends PSym("-")   with PSymbolOp with PUnaryOp {
     override def signatures = List(
-      Map(POpApp.pArgS(0) -> Int, POpApp.pResS -> Int),
-      Map(POpApp.pArgS(0) -> Perm, POpApp.pResS -> Perm))
+      Map(POpApp.pArgS(0) -> Perm, POpApp.pResS -> Perm),
+      Map(POpApp.pArgS(0) -> Int, POpApp.pResS -> Int))
   }
   case object Not     extends PSym("!")   with PSymbolOp with PUnaryOp {
     override def signatures = List(Map(POpApp.pArgS(0) -> Bool, POpApp.pResS -> Bool))

Diff for: src/test/resources/all/issues/silver/0745.vpr

@@ -0,0 +1,29 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+method doubleDiv(r: Ref)
+{
+    inhale acc(r.f, 1 / 4000 / 2)
+    var tmp: Int
+    tmp := r.f
+}
+
+method compare(r: Ref)
+{
+    assert 0 / 1 < 1 / 2
+    assert !(0 \ 1 < 1 \ 2)
+
+    assert 1 / 2 > 0 / 1
+    assert !(1 \ 2 > 0 \ 1)
+
+    assert !(0 / 1 >= 1 / 2)
+    assert (0 \ 1 >= 1 \ 2)
+
+    assert 0 / 1 != 1 / 2
+    assert !(0 / 1 == 1 / 2)
+
+    assert 0 \ 1 == 1 \ 2
+    assert !(0 \ 1 != 1 \ 2)
+}