Merge pull request #192 from PascalDevenoge/improved_real_float_modeling

Improved real float modeling
marcoeilers · May 28, 2024 · 5682954 · 5682954
2 parents d14145a + 25f28f1
commit 5682954
Show file tree

Hide file tree

Showing 13 changed files with 775 additions and 78 deletions.
diff --git a/src/nagini_contracts/contracts.py b/src/nagini_contracts/contracts.py
@@ -31,7 +31,7 @@
                   'Acc', 'Rd', 'Wildcard', 'Fold', 'Unfold', 'Unfolding', 'Previous',
                   'RaisedException', 'PSeq', 'PSet', 'ToSeq', 'ToMS', 'MaySet', 'MayCreate',
                   'getMethod', 'getArg', 'getOld', 'arg', 'Joinable', 'MayStart', 'Let',
-                  'PMultiset', 'LowExit', 'Refute']
+                  'PMultiset', 'LowExit', 'Refute', 'isNaN']
 
 T = TypeVar('T')
 V = TypeVar('V')
@@ -506,6 +506,8 @@ def dict_pred(d: object) -> bool:
     be folded or unfolded.
     """
 
+def isNaN(f: float) -> bool:
+    pass
 
 __all__ = [
         'Requires',
@@ -560,4 +562,5 @@ def dict_pred(d: object) -> bool:
         'ToMS',
         'MaySet',
         'MayCreate',
+        'isNaN'
         ]
diff --git a/src/nagini_translation/lib/resolver.py b/src/nagini_translation/lib/resolver.py
@@ -461,7 +461,7 @@ def _get_call_type(node: ast.Call, module: PythonModule,
                 return ctx.current_contract_exception
             elif node.func.id in ('Acc', 'Rd', 'Read', 'Implies', 'Forall', 'IOForall', 'Exists',
                                   'Forall2', 'Forall3', 'Forall4', 'Forall5', 'Forall6',
-                                  'MayCreate', 'MaySet', 'Low', 'LowVal', 'LowEvent', 'LowExit'):
+                                  'MayCreate', 'MaySet', 'Low', 'LowVal', 'LowEvent', 'LowExit', 'isNaN'):
                 return module.global_module.classes[BOOL_TYPE]
             elif node.func.id == 'Declassify':
                 return None

diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil
@@ -40,6 +40,7 @@ function int___unbox__(box: Ref): Int
     requires issubtype(typeof(box), int())
     ensures !issubtype(typeof(box), bool()) ==> __prim__int___box__(result) == box
     ensures issubtype(typeof(box), bool()) ==> __prim__bool___box__(result != 0) == box
+    ensures forall i: Ref :: {object___eq__(box, i), int___unbox__(i)} (object___eq__(box, i) && issubtype(typeof(i), int())) ==> int___unbox__(i) == result
 
 function __prim__bool___box__(prim: Bool): Ref
     decreases _
@@ -55,9 +56,10 @@ function bool___unbox__(box: Ref): Bool
 function int___eq__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), int())
-    requires issubtype(typeof(other), int())
-    ensures result == int___unbox__(self) == int___unbox__(other)
-    ensures result == object___eq__(self, other)
+    requires issubtype(typeof(other), int()) || issubtype(typeof(other), float())
+    ensures issubtype(typeof(other), int()) ==> result == int___unbox__(self) == int___unbox__(other)
+    ensures issubtype(typeof(other), int()) ==> result == object___eq__(self, other)
+    ensures issubtype(typeof(other), float()) ==> result == float___eq__(self, other)
 
 
 function bool___eq__(self: Ref, other: Ref): Bool

diff --git a/src/nagini_translation/resources/float.sil b/src/nagini_translation/resources/float.sil
@@ -9,6 +9,11 @@ function float___bool__(self: Ref): Bool
     ensures self == null ==> !result
     ensures issubtype(typeof(self), int()) ==> (result == int___bool__(self))
 
+function float___isNaN(f: Ref): Bool
+    decreases _
+    requires issubtype(typeof(f), float())
+    ensures issubtype(typeof(f), int()) ==> result == false
+
 function float___ge__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), float())

diff --git a/src/nagini_translation/resources/float_ieee32.sil b/src/nagini_translation/resources/float_ieee32.sil
@@ -18,6 +18,11 @@ function float___bool__(self: Ref): Bool
     ensures self == null ==> !result
     ensures result == (float___unbox__(self) != ___float32_zero())
 
+function float___isNaN(f: Ref): Bool
+    decreases _
+    requires issubtype(typeof(f), float())
+    ensures result == ___float32_isNaN(float___unbox__(f)) 
+
 function float___ge__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), float())
@@ -144,6 +149,7 @@ domain ___float32 interpretation (Boogie: "float24e8", SMTLIB: "(_ FloatingPoint
   function real____to_int(p: Perm): Int interpretation "to_int"
   function ___float32_to_real(p: ___float32): Perm interpretation "fp.to_real"
   function ___float32_NaN(): ___float32 interpretation "(_ NaN 8 24)"
+  function ___float32_isNaN(___float32): Bool interpretation "fp.isNaN"
 }
 
 function ___float32_zero(): ___float32

diff --git a/src/nagini_translation/resources/float_real.sil b/src/nagini_translation/resources/float_real.sil
diff --git a/src/nagini_translation/resources/preamble.index b/src/nagini_translation/resources/preamble.index
@@ -226,7 +226,7 @@
         "__eq__": {
             "args": ["int", "object"],
             "type": "__prim__bool",
-            "requires": ["__unbox__"]
+            "requires": ["__unbox__", "float___eq__"]
         },
         "__add__": {
             "args": ["__prim__int", "__prim__int"],
@@ -304,77 +304,97 @@
         "__unbox__": {
             "args": ["float"],
             "type": "__prim__perm",
-            "requires": ["int___unbox__"]
+            "requires": ["int___unbox__", "float___is_nan__", "float___is_inf__"]
+        },
+        "__box_nan": {
+            "args": [],
+            "type": "float",
+            "requires": ["float___is_nan__", "float___is_inf__"]
+        },
+        "__box_inf": {
+            "args": ["__prim__bool"],
+            "type": "float",
+            "requires": ["float___is_nan__", "float___is_inf__"]
+        },
+        "__is_nan__": {
+            "args": ["float"],
+            "type": "__prim__bool",
+            "requires": []
+        },
+        "__is_inf__": {
+            "args": ["float", "__prim__bool"],
+            "type": "__prim__bool",
+            "requires": []
         },
         "__bool__": {
             "args": ["float"],
             "type": "__prim__bool",
-            "requires": ["int___bool__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"]
+            "requires": ["int___bool__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero", "float___is_nan__", "float___is_inf__"]
         },
         "__eq__": {
             "args": ["float", "object"],
             "type": "__prim__bool",
-            "requires": ["int___eq__", "unbox"]
+            "requires": ["int___eq__", "unbox", "float___is_nan__", "float___is_inf__"]
         },
         "__add__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___add__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___add__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__radd__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___add__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___add__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__sub__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___sub__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___sub__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__rsub__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___sub__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___sub__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__mul__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___mul__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___mul__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__rmul__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___mul__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___mul__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__truediv__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"]
+            "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__rtruediv__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"]
+            "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__ge__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___ge__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___ge__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__gt__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___gt__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___gt__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__lt__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___lt__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___lt__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__le__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___le__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___le__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__pos__": {
             "args": ["float"],
@@ -384,12 +404,17 @@
         "__neg__": {
             "args": ["float"],
             "type": "float",
-            "requires": ["int___neg__", "__prim__perm___box__", "unbox"]
+            "requires": ["int___neg__", "__prim__perm___box__", "unbox", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__int__": {
             "args": ["float"],
             "type": "int",
-            "requires": ["unbox", "__prim__int___box__"]
+            "requires": ["unbox", "__prim__int___box__", "float___is_nan__", "float___is_inf__"]
+        },
+        "__isNaN": {
+            "args": ["float"],
+            "type": "__prim__bool",
+            "requires": ["float___is_nan__", "float___unbox__"]
         }
     },
     "extends": "object"
@@ -632,7 +657,7 @@
         "__box__": {
             "args": ["__prim__perm"],
             "type": "int",
-            "requires": ["float___unbox__"]
+            "requires": ["float___unbox__", "float___is_nan__", "float___is_inf__"]
         }
     }
 },

diff --git a/src/nagini_translation/sif/resources/preamble.index b/src/nagini_translation/sif/resources/preamble.index
@@ -229,7 +229,7 @@
         "__eq__": {
             "args": ["int", "object"],
             "type": "__prim__bool",
-            "requires": ["__unbox__"]
+            "requires": ["__unbox__", "float___eq__"]
         },
         "__add__": {
             "args": ["__prim__int", "__prim__int"],
@@ -303,6 +303,31 @@
             "args": ["__prim__int"],
             "type": "float"
         },
+        "__unbox__": {
+            "args": ["float"],
+            "type": "__prim__perm",
+            "requires": ["int___unbox__", "float___is_nan__", "float___is_inf__"]
+        },
+        "__box_nan": {
+            "args": [],
+            "type": "float",
+            "requires": ["float___is_nan__", "float___is_inf__"]
+        },
+        "__box_inf": {
+            "args": ["__prim__bool"],
+            "type": "float",
+            "requires": ["float___is_nan__", "float___is_inf__"]
+        },
+        "__is_nan__": {
+            "args": ["float"],
+            "type": "__prim__bool",
+            "requires": []
+        },
+        "__is_inf__": {
+            "args": ["float", "__prim__bool"],
+            "type": "__prim__bool",
+            "requires": []
+        },
         "__bool__": {
             "args": ["float"],
             "type": "__prim__bool",
@@ -311,47 +336,67 @@
         "__eq__": {
             "args": ["float", "object"],
             "type": "__prim__bool",
-            "requires": ["int___eq__"]
+            "requires": ["int___eq__", "unbox", "float___is_nan__", "float___is_inf__"]
         },
         "__add__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___add__", "int___unbox__"]
+            "requires": ["int___add__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
+        },
+        "__radd__": {
+            "args": ["float", "float"],
+            "type": "float",
+            "requires": ["int___add__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__sub__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___sub__", "int___unbox__"]
+            "requires": ["int___sub__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
+        },
+        "__rsub__": {
+            "args": ["float", "float"],
+            "type": "float",
+            "requires": ["int___sub__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__mul__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___mul__", "int___unbox__"]
+            "requires": ["int___mul__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
+        },
+        "__rmul__": {
+            "args": ["float", "float"],
+            "type": "float",
+            "requires": ["int___mul__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__truediv__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___truediv__", "int___unbox__"]
+            "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
+        },
+        "__rtruediv__": {
+            "args": ["float", "float"],
+            "type": "float",
+            "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__ge__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___ge__", "int___unbox__"]
+            "requires": ["int___ge__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__gt__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___gt__", "int___unbox__"]
+            "requires": ["int___gt__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__lt__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___lt__", "int___unbox__"]
+            "requires": ["int___lt__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__le__": {
             "args": ["float", "float"],
             "type": "__prim__bool",
-            "requires": ["int___le__", "int___unbox__"]
+            "requires": ["int___le__", "int___unbox__", "unbox", "__prim__perm___box__", "float___is_nan__", "float___is_inf__"]
         },
         "__pos__": {
             "args": ["float"],
@@ -361,11 +406,12 @@
         "__neg__": {
             "args": ["float"],
             "type": "float",
-            "requires": ["int___neg__", "__prim__perm___box__", "unbox"]
+            "requires": ["int___neg__", "__prim__perm___box__", "unbox", "float___is_nan__", "float___box_nan", "float___is_inf__", "float___box_inf"]
         },
         "__int__": {
             "args": ["float"],
-            "type": "int"
+            "type": "int",
+            "requires": ["unbox", "__prim__int___box__", "float___is_nan__", "float___is_inf__"]
         }
     },
     "extends": "object"