Tests, outputting warnings when uninterpreted floats are used

src/nagini_translation/conftest.py

@@ -250,10 +250,18 @@ def pytest_generate_tests(metafunc: 'pytest.python.Metafunc'):
             files = _test_files(test_dir)
             test_files.extend(files)
             reload_triggers.add(files[0])
+            print(files[0])
         if _pytest_config.single_test and 'verification' in _pytest_config.single_test:
             test_files.append(_pytest_config.single_test)
+        float_encoding = None
         for file in test_files:
             ignore_obligations = 'no_obligations' in file
+            if 'float_real' in file:
+                new_float_encoding = 'real'
+            elif 'float_ieee32' in file:
+                new_float_encoding = 'ieee32'
+            else:
+                new_float_encoding = None
             if 'sif-true' in file:
                 sif = True
             elif 'sif-poss' in file:
@@ -264,12 +272,14 @@ def pytest_generate_tests(metafunc: 'pytest.python.Metafunc'):
                 sif = False
             if _pytest_config.force_product:
                 sif = True
-            reload_resources = file in reload_triggers
+            reload_resources = (file in reload_triggers) or (new_float_encoding != float_encoding)
+            float_encoding = new_float_encoding
             arp = 'arp' in file
             base = file.partition('verification')[0] + 'verification'
-            params.extend([(file, base, verifier, sif, reload_resources, arp, ignore_obligations, _pytest_config.store_viper) for verifier
+            params.extend([(file, base, verifier, sif, reload_resources, arp, ignore_obligations,
+                            _pytest_config.store_viper, float_encoding) for verifier
                            in _pytest_config.verifiers])
-        metafunc.parametrize('path,base,verifier,sif,reload_resources,arp,ignore_obligations,print', params)
+        metafunc.parametrize('path,base,verifier,sif,reload_resources,arp,ignore_obligations,print,float_encoding', params)
     else:
         pytest.exit('Unrecognized test function.')
 

src/nagini_translation/resources/float_ieee32.sil

@@ -92,8 +92,6 @@ domain ___float32 interpretation (Boogie: "float24e8", SMTLIB: "(_ FloatingPoint
   function ___float32_from_real(r: Perm): ___float32 interpretation "(_ to_fp 8 24) RNE"
   function ___float32_eq(___float32, ___float32): Bool interpretation "fp.eq"
 
-  //function ___float32_fp_min(f1: ___float32, f2: ___float32): ___float32 interpretation "fp.min"
-  //function ___float32_fp_max(f1: ___float32, f2: ___float32): ___float32 interpretation "fp.max"
   function ___float32_add(d1: ___float32, f2: ___float32): ___float32 interpretation "fp.add RNE"
   function ___float32_sub(d1: ___float32, f2: ___float32): ___float32 interpretation "fp.sub RNE"
   function ___float32_mul(d1: ___float32, f2: ___float32): ___float32 interpretation "fp.mul RNE"
@@ -103,6 +101,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_zero(): ___float32

src/nagini_translation/tests.py

@@ -558,7 +558,8 @@ class VerificationTest(AnnotatedTest):
 
     def test_file(
             self, path: str, base: str, jvm: jvmaccess.JVM, verifier: ViperVerifier,
-            sif: bool, reload_resources: bool, arp: bool, ignore_obligations: bool, store_viper: bool):
+            sif: bool, reload_resources: bool, arp: bool, ignore_obligations: bool, store_viper: bool,
+            float_encoding: Optional[str]):
         """Test specific Python file."""
         config.obligation_config.disable_all = ignore_obligations
         annotation_manager = self.get_annotation_manager(path, verifier.name)
@@ -568,7 +569,8 @@ def test_file(
             pytest.skip('Ignored')
         abspath = os.path.abspath(path)
         absbase = os.path.abspath(base)
-        modules, prog = translate(abspath, jvm, base_dir=absbase, sif=sif, arp=arp, reload_resources=reload_resources)
+        modules, prog = translate(abspath, jvm, base_dir=absbase, sif=sif, arp=arp, reload_resources=reload_resources,
+                                  float_encoding=float_encoding)
         assert prog is not None
         if store_viper:
             import string
@@ -618,9 +620,10 @@ def _evaluate_result(
 _VERIFICATION_TESTER = VerificationTest()
 
 
-def test_verification(path, base, verifier, sif, reload_resources, arp, ignore_obligations, print):
+def test_verification(path, base, verifier, sif, reload_resources, arp, ignore_obligations, print, float_encoding):
     """Execute provided verification test."""
-    _VERIFICATION_TESTER.test_file(path, base, _JVM, verifier, sif, reload_resources, arp, ignore_obligations, print)
+    _VERIFICATION_TESTER.test_file(path, base, _JVM, verifier, sif, reload_resources, arp, ignore_obligations,
+                                   print, float_encoding)
 
 
 class TranslationTest(AnnotatedTest):

src/nagini_translation/translators/common.py

@@ -13,6 +13,7 @@
     ASSERTING_FUNC,
     COMBINE_NAME_FUNC,
     DICT_TYPE,
+    FLOAT_TYPE,
     INT_TYPE,
     IS_DEFINED_FUNC,
     LIST_TYPE,
@@ -710,6 +711,11 @@ def get_function_call(self, receiver: PythonType,
             return chain_cond_exp(guarded_functions, self.viper, position,
                                   self.no_info(ctx), ctx)
         else:
+            if receiver.python_class.name == FLOAT_TYPE:
+                if ctx.float_encoding is None:
+                    import logging
+                    logging.warning("Floating point operations are uninterpreted by default. To use interpreted "
+                                    "floating point operations, use option --float-encoding")
             # Pass-through
             return self._get_function_call(receiver, func_name, args,
                                            arg_types, node, ctx, position)

src/nagini_translation/translators/expression.py

@@ -265,6 +265,9 @@ def translate_Num(self, node: ast.Num, ctx: Context) -> StmtsAndExpr:
                                                [None], node, ctx, pos)
             return [], float_val
         if isinstance(node.n, float):
+            import logging
+            logging.warning("Floating point operations are uninterpreted by default. To use interpreted "
+                            "floating point operations, use option --float-encoding")
             float_class = ctx.module.global_module.classes[FLOAT_TYPE]
             index_lit = self.viper.IntLit(ctx.get_fresh_int(), pos, info)
             float_val = self.get_function_call(float_class, '__create__', [index_lit],

tests/functional/verification/float_ieee32/test_float.py

@@ -0,0 +1,61 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+#:: IgnoreFile(carbon)(158)
+
+from nagini_contracts.contracts import *
+
+def useOps(f: float, g: float) -> float:
+    a = f - g
+    b = f * g
+    c = f > g
+    d = f >= g
+    e = f < g
+    e2 = f <= g
+    return f
+
+
+def cmpLits() -> None:
+    Assert(3.0 > 2.0)
+    Assert(1.0 <= 40.0)
+
+def sqr3(num : float) -> float:
+    Requires(num >= 0.0)
+    #:: ExpectedOutput(postcondition.violated:assertion.false)
+    Ensures(Result() > 0.0)
+    Ensures(num * num == Result())
+    return num * num
+
+def arith(num: float) -> float:
+    Requires(num == num)  # not NaN
+    Ensures(Result() == num + 3.0)
+    tmp = 1.0 + 2.0
+    return num + tmp
+
+
+def arith3(num: float) -> float:
+    #:: ExpectedOutput(postcondition.violated:assertion.false)
+    Ensures(Result() == num + 3.0)
+    return num + 3.0
+
+
+def arith2(num: float) -> float:
+    Requires(num == num)  # not NaN
+    #:: ExpectedOutput(postcondition.violated:assertion.false)
+    Ensures(Result() == num + 4.0)
+    return num + 1.0 + 2.0
+
+
+def intComp() -> None:
+    a = 3.0
+    b = 3
+    #:: UnexpectedOutput(assert.failed:assertion.false,158)
+    Assert(a == b)
+
+def divSave(f: float, g: float) -> float:
+    #:: ExpectedOutput(application.precondition:assertion.false)
+    return f / g
+
+def divSave2(f: float, g: float) -> float:
+    Requires(g != 0.0)
+    return f / g

tests/functional/verification/float_real/test_float.py

@@ -0,0 +1,66 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+
+from nagini_contracts.contracts import *
+
+
+def useOps(f: float, g: float) -> float:
+    a = f - g
+    b = f * g
+    c = f > g
+    d = f >= g
+    e = f < g
+    e2 = f <= g
+    return f
+
+
+def cmpLits() -> None:
+    Assert(3.0 > 2.0)
+    Assert(1.0 <= 40.0)
+
+def sqr(num : float) -> float:
+    Requires(num >= 0)
+    Ensures(Result() >= 0)
+    Ensures(num * num == Result())
+    return num * num
+
+
+def sqr2(num : float) -> float:
+    Requires(num >= 0.0)
+    Ensures(Result() >= 0.0)
+    Ensures(num * num == Result())
+    return num * num
+
+
+def sqr3(num : float) -> float:
+    Requires(num >= 0.0)
+    #:: ExpectedOutput(postcondition.violated:assertion.false)
+    Ensures(Result() > 0.0)
+    Ensures(num * num == Result())
+    return num * num
+
+def arith(num: float) -> float:
+    Ensures(Result() == num + 3)
+    return num + 1.0 + 2.0
+
+
+def arith2(num: float) -> float:
+    #:: ExpectedOutput(postcondition.violated:assertion.false)
+    Ensures(Result() == num + 4)
+    return num + 1.0 + 2.0
+
+
+def intComp() -> None:
+    a = 3.0
+    b = 3
+    Assert(a == b)
+
+def divSave(f: float, g: float) -> float:
+    #:: ExpectedOutput(application.precondition:assertion.false)
+    tmp = f / g
+    return 1.0
+
+def divSave2(f: float, g: float) -> float:
+    Requires(g != 0.0)
+    return f / g