Merge branch 'master' into py310

marcoeilers · Apr 28, 2024 · f2ee2e3 · f2ee2e3
2 parents 184a0e5 + 9ee9d5f
commit f2ee2e3
Show file tree

Hide file tree

Showing 7 changed files with 27 additions and 25 deletions.
diff --git a/src/nagini_translation/lib/constants.py b/src/nagini_translation/lib/constants.py
@@ -218,20 +218,22 @@
     '__add__',
     '__sub__',
     '__mul__',
+    '__matmul__',
     '__truediv__',
     '__floordiv__',
     '__mod__',
-    '__neg__',
-    '__pos__',
-    '__invert__',
-
     '__divmod__',
     '__pow__',
     '__lshift__',
     '__rshift__',
     '__and__',
     '__or__',
     '__xor__',
+
+    '__neg__',
+    '__pos__',
+    '__invert__',
+
 
     '__radd__',
     '__rsub__',
@@ -262,7 +264,7 @@
     '__isub__',
     '__imul__',
     '__imatmul__',
-    '__idiv__',
+    '__itruediv__',
     '__ifloordiv__',
     '__imod__',
     '__ipow__',
@@ -378,7 +380,7 @@
     ast.Sub: '__sub__',
     ast.Mult: '__mul__',
     ast.MatMult: '__matmul__',
-    ast.Div: '__div__',
+    ast.Div: '__truediv__',
     ast.FloorDiv: '__floordiv__',
     ast.Mod: '__mod__',
     ast.Pow: '__pow__',
@@ -394,7 +396,7 @@
     ast.Sub: '__isub__',
     ast.Mult: '__imul__',
     ast.MatMult: '__imatmul__',
-    ast.Div: '__idiv__',
+    ast.Div: '__itruediv__',
     ast.FloorDiv: '__ifloordiv__',
     ast.Mod: '__imod__',
     ast.Pow: '__ipow__',
@@ -410,7 +412,7 @@
     ast.Sub: '__rsub__',
     ast.Mult: '__rmul__',
     ast.MatMult: '__rmatmul__',
-    ast.Div: '__rdiv__',
+    ast.Div: '__rtruediv__',
     ast.FloorDiv: '__rfloordiv__',
     ast.Mod: '__rmod__',
     ast.Pow: '__rpow__',

diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil
@@ -133,7 +133,7 @@ function int___floordiv__(self: Int, other: Int): Int
     self \ other
 }
 
-function int___div__(self: Int, other: Int): Ref
+function int___truediv__(self: Int, other: Int): Ref
     decreases _
     requires @error("Divisor may be zero.")(other != 0)
     ensures (self % other == 0) ==> (typeof(result) == int() && int___unbox__(result) == self \ other)

diff --git a/src/nagini_translation/resources/float.sil b/src/nagini_translation/resources/float.sil
@@ -92,15 +92,15 @@ function float___rmul__(self: Ref, other: Ref): Ref
     ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==>
             (result == __prim__int___box__(int___mul__(int___unbox__(other), int___unbox__(self))))
 
-function float___div__(self: Ref, other: Ref): Ref
+function float___truediv__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
     requires issubtype(typeof(other), int()) ==> int___unbox__(other) != 0
     requires issubtype(typeof(other), int())  // cannot express non-zero at the moment
     ensures issubtype(typeof(result), float())
     ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==>
-            (result == int___div__(int___unbox__(self), int___unbox__(other)))
+            (result == int___truediv__(int___unbox__(self), int___unbox__(other)))
 
 function float___pos__(self: Ref): Ref
     decreases _
@@ -114,15 +114,15 @@ function float___neg__(self: Ref): Ref
     ensures issubtype(typeof(result), float())
     ensures issubtype(typeof(self), int()) ==> result == int___neg__(self)
 
-function float___rdiv__(self: Ref, other: Ref): Ref
+function float___rtruediv__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
     requires issubtype(typeof(self), int()) ==> int___unbox__(self) != 0
     requires issubtype(typeof(self), int())  // cannot express non-zero at the moment
     ensures issubtype(typeof(result), float())
     ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==>
-            (result == int___div__(int___unbox__(other), int___unbox__(self)))
+            (result == int___truediv__(int___unbox__(other), int___unbox__(self)))
 
 function float___int__(self: Ref): Ref
     decreases _

diff --git a/src/nagini_translation/resources/float_ieee32.sil b/src/nagini_translation/resources/float_ieee32.sil
@@ -90,7 +90,7 @@ function float___rmul__(self: Ref, other: Ref): Ref
     ensures issubtype(typeof(result), float())
     ensures result == __prim__perm___box__(___float32_mul(float___unbox__(other), float___unbox__(self)))
 
-function float___div__(self: Ref, other: Ref): Ref
+function float___truediv__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
@@ -110,7 +110,7 @@ function float___neg__(self: Ref): Ref
     ensures issubtype(typeof(result), float())
     ensures result == __prim__perm___box__(___float32_neg(float___unbox__(self)))
 
-function float___rdiv__(self: Ref, other: Ref): Ref
+function float___rtruediv__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())

diff --git a/src/nagini_translation/resources/float_real.sil b/src/nagini_translation/resources/float_real.sil
@@ -90,7 +90,7 @@ function float___rmul__(self: Ref, other: Ref): Ref
     ensures issubtype(typeof(result), float())
     ensures result == __prim__perm___box__(float___unbox__(other) * float___unbox__(self))
 
-function float___div__(self: Ref, other: Ref): Ref
+function float___truediv__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
@@ -109,7 +109,7 @@ function float___neg__(self: Ref): Ref
     ensures issubtype(typeof(result), float())
     ensures result == __prim__perm___box__(-float___unbox__(self))
 
-function float___rdiv__(self: Ref, other: Ref): Ref
+function float___rtruediv__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())

diff --git a/src/nagini_translation/resources/preamble.index b/src/nagini_translation/resources/preamble.index
@@ -241,7 +241,7 @@
             "args": ["__prim__int", "__prim__int"],
             "type": "__prim__int"
         },
-        "__div__": {
+        "__truediv__": {
             "args": ["__prim__int", "__prim__int"],
             "type": "float"
         },
@@ -346,15 +346,15 @@
             "type": "float",
             "requires": ["int___mul__", "int___unbox__", "unbox", "__prim__perm___box__"]
         },
-        "__div__": {
+        "__truediv__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___div__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"]
+            "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"]
         },
-        "__rdiv__": {
+        "__rtruediv__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___div__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"]
+            "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"]
         },
         "__ge__": {
             "args": ["float", "float"],

diff --git a/src/nagini_translation/sif/resources/preamble.index b/src/nagini_translation/sif/resources/preamble.index
@@ -244,7 +244,7 @@
             "args": ["__prim__int", "__prim__int"],
             "type": "__prim__int"
         },
-        "__div__": {
+        "__truediv__": {
             "args": ["__prim__int", "__prim__int"],
             "type": "float"
         },
@@ -328,10 +328,10 @@
             "type": "float",
             "requires": ["int___mul__", "int___unbox__"]
         },
-        "__div__": {
+        "__truediv__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___div__", "int___unbox__"]
+            "requires": ["int___truediv__", "int___unbox__"]
         },
         "__ge__": {
             "args": ["float", "float"],