Merge pull request #194 from marcoeilers/master

Merge

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'
         ]

src/nagini_translation/lib/errors/messages.py

@@ -99,6 +99,8 @@
         lambda n: 'Divisor {} might be zero.'.format(pprint(n)),
     'negative.permission':
         lambda n: 'Fraction {} might be negative.'.format(pprint(n)),
+    'permission.not.positive':
+        lambda n: 'Fraction {} might not be positive'.format(pprint(n)),
     'insufficient.permission':
         lambda n: ('There might be insufficient permission to '
                    'access {}.').format(pprint(n)),
@@ -203,6 +205,7 @@
     'receiver.null': 'Receiver might be null.',
     'division.by.zero': 'Divisor might be zero.',
     'negative.permission': 'Fraction might be negative.',
+    'permission.not.positive': 'Fraction might not be positive.',
     'insufficient.permission': 'There might be insufficient permission.',
     'termination_measure.non_positive': 'Termination measure might be non-positive.',
     'measure.non_decreasing': 'Termination measure might not be smaller.',

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

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

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())

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