Floats from string literals, tests

src/nagini_translation/conftest.py

@@ -232,6 +232,12 @@ def pytest_generate_tests(metafunc: 'pytest.python.Metafunc'):
         if _pytest_config.single_test and 'translation' in _pytest_config.single_test:
             test_files.append(_pytest_config.single_test)
         for file in test_files:
+            if 'float_real' in file:
+                float_encoding = 'real'
+            elif 'float_ieee32' in file:
+                float_encoding = 'ieee32'
+            else:
+                float_encoding = None
             if 'sif-true' in file:
                 sif = True
             elif 'sif-poss' in file:
@@ -243,8 +249,8 @@ def pytest_generate_tests(metafunc: 'pytest.python.Metafunc'):
             reload_resources = file in reload_triggers
             arp = 'arp' in file
             base = file.partition('translation')[0] + 'translation'
-            params.append((file, base, sif, reload_resources, arp))
-        metafunc.parametrize('path,base,sif,reload_resources,arp', params)
+            params.append((file, base, sif, reload_resources, arp, float_encoding))
+        metafunc.parametrize('path,base,sif,reload_resources,arp,float_encoding', params)
     elif func_name == _VERIFICATION_TEST_FUNCTION_NAME:
         for test_dir in _pytest_config.verification_test_dirs:
             files = _test_files(test_dir)

src/nagini_translation/lib/constants.py

@@ -15,6 +15,7 @@
 
 BUILTINS = ['cast',
             'int',
+            'float',
             'isinstance',
             'bool',
             'len',

src/nagini_translation/tests.py

@@ -630,15 +630,16 @@ class TranslationTest(AnnotatedTest):
     """Test for testing translation errors."""
 
     def test_file(self, path: str, base: str, jvm: jvmaccess.JVM, sif: bool,
-                  reload_resources: bool, arp: bool):
+                  reload_resources: bool, arp: bool, float_encoding: Optional[str]):
         """Test specific Python file."""
         annotation_manager = self.get_annotation_manager(path, _BACKEND_ANY)
         if annotation_manager.ignore_file():
             pytest.skip('Ignored')
         path = os.path.abspath(path)
         base = os.path.abspath(base)
         try:
-            translate(path, jvm, base_dir=base, sif=sif, arp=arp, reload_resources=reload_resources)
+            translate(path, jvm, base_dir=base, sif=sif, arp=arp, reload_resources=reload_resources,
+                      float_encoding=float_encoding)
             actual_errors = []
         except InvalidProgramException as exp1:
             actual_errors = [InvalidProgramError(exp1)]
@@ -654,6 +655,6 @@ def test_file(self, path: str, base: str, jvm: jvmaccess.JVM, sif: bool,
 _TRANSLATION_TESTER = TranslationTest()
 
 
-def test_translation(path, base, sif, reload_resources, arp):
+def test_translation(path, base, sif, reload_resources, arp, float_encoding):
     """Execute provided translation test."""
-    _TRANSLATION_TESTER.test_file(path, base, _JVM, sif, reload_resources, arp)
+    _TRANSLATION_TESTER.test_file(path, base, _JVM, sif, reload_resources, arp, float_encoding)

src/nagini_translation/translators/abstract.py

@@ -349,6 +349,9 @@ def translate_finally(self, block: PythonTryBlock,
                           ctx: Context) -> List[Stmt]:
         return self.config.method_translator.translate_finally(block, ctx)
 
+    def translate_float_literal(self, lit: float, node: ast.AST, ctx: Context) -> Expr:
+        return self.config.expr_translator.translate_float_literal(lit, node, ctx)
+
     def type_check(self, lhs: Expr, type: PythonType,
                    position: 'silver.ast.Position', ctx: Context,
                    inhale_exhale: bool=True) -> Expr:

src/nagini_translation/translators/call.py

@@ -143,6 +143,18 @@ def _translate_int(self, node: ast.Call, ctx: Context) -> StmtsAndExpr:
                                                          [None], node, ctx)
         return stmt + str_stmt, str_val
 
+    def _translate_float(self, node: ast.Call, ctx: Context) -> StmtsAndExpr:
+        assert len(node.args) == 1
+        if isinstance(node.args[0], ast.Str):
+            string_val = node.args[0].s
+            try:
+                float_val = float(string_val)
+                return [], self.translate_float_literal(float_val, node, ctx)
+            except ValueError:
+                raise InvalidProgramException(node, 'invalid.float.val')
+        msg = 'float() is currently only supported with arguments NaN and inf.'
+        raise UnsupportedException(node, msg)
+
     def _translate_bool(self, node: ast.Call, ctx: Context) -> StmtsAndExpr:
         assert len(node.args) == 1
         stmt, target = self.translate_expr(node.args[0], ctx)
@@ -486,6 +498,8 @@ def _translate_builtin_func(self, node: ast.Call,
             return self._translate_str(node, ctx)
         elif func_name == 'int':
             return self._translate_int(node, ctx)
+        elif func_name == 'float':
+            return self._translate_float(node, ctx)
         elif func_name == 'bool':
             return self._translate_bool(node, ctx)
         elif func_name == 'set':

src/nagini_translation/translators/expression.py

@@ -246,34 +246,46 @@ def translate_Num(self, node: ast.Num, ctx: Context) -> StmtsAndExpr:
             boxed_lit = self.get_function_call(int_class, '__box__', [lit],
                                                [None], node, ctx)
             return [], boxed_lit
-        if isinstance(node.n, float) and ctx.float_encoding == "real":
+        if isinstance(node.n, float):
+            return [], self.translate_float_literal(node.n, node, ctx)
+        raise UnsupportedException(node, 'Unsupported number literal')
+
+    def translate_float_literal(self, lit: float, node: ast.AST, ctx: Context) -> Expr:
+        pos = self.to_position(node, ctx)
+        info = self.no_info(ctx)
+        if ctx.float_encoding == "real":
             prim_perm_class = ctx.module.global_module.classes[PRIMITIVE_PERM_TYPE]
-            num, den = node.n.as_integer_ratio()
-            num_lit = self.viper.IntLit(num, pos, info)
-            den_lit = self.viper.IntLit(den, pos, info)
-            frac = self.viper.FractionalPerm(num_lit, den_lit, pos, info)
-            float_val = self.get_function_call(prim_perm_class, '__box__', [frac],
-                                               [None], node, ctx, pos)
-            return [], float_val
-        if isinstance(node.n, float) and ctx.float_encoding == "ieee32":
+            try:
+                num, den = lit.as_integer_ratio()
+                num_lit = self.viper.IntLit(num, pos, info)
+                den_lit = self.viper.IntLit(den, pos, info)
+                frac = self.viper.FractionalPerm(num_lit, den_lit, pos, info)
+                float_val = self.get_function_call(prim_perm_class, '__box__', [frac],
+                                                   [None], node, ctx, pos)
+                return float_val
+            except ValueError:
+                # NaN
+                raise InvalidProgramException(node, 'non.real.float')
+            except OverflowError:
+                # Inf
+                raise InvalidProgramException(node, 'non.real.float')
+        if ctx.float_encoding == "ieee32":
             float_class = ctx.module.global_module.classes[FLOAT_TYPE]
             import struct
-            bytes_val = struct.pack('!f', node.n)
+            bytes_val = struct.pack('!f', lit)
             int_val = int.from_bytes(bytes_val, "big")
             int_lit = self.viper.IntLit(int_val, pos, info)
             float_val = self.get_function_call(float_class, '__create__', [int_lit],
                                                [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],
-                                               [None], node, ctx, pos)
-            return [], float_val
-        raise UnsupportedException(node, 'Unsupported number literal')
+            return float_val
+        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],
+                                           [None], node, ctx, pos)
+        return float_val
 
     def translate_Dict(self, node: ast.Dict, ctx: Context) -> StmtsAndExpr:
         args = []

tests/functional/translation/float_ieee32/test_non_float.py

@@ -0,0 +1,13 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+from nagini_contracts.contracts import *
+
+def specialVals() -> None:
+    #:: ExpectedOutput(invalid.program:invalid.float.val)
+    nan = float("asdasd")
+    nf = float("inF")
+    one = float("1.0")
+    Assert(nf > one)
+    Assert(not nan == nan)
+    Assert(nan == nan)

tests/functional/translation/float_real/test_non_float.py

@@ -0,0 +1,13 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+from nagini_contracts.contracts import *
+
+def specialVals() -> None:
+    #:: ExpectedOutput(invalid.program:invalid.float.val)
+    nan = float("asdasd")
+    nf = float("inF")
+    one = float("1.0")
+    Assert(nf > one)
+    Assert(not nan == nan)
+    Assert(nan == nan)

tests/functional/translation/float_real/test_non_real.py

@@ -0,0 +1,13 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+from nagini_contracts.contracts import *
+
+def specialVals() -> None:
+    #:: ExpectedOutput(invalid.program:non.real.float)
+    nan = float("nan")
+    nf = float("inF")
+    one = float("1.0")
+    Assert(nf > one)
+    Assert(not nan == nan)
+    Assert(nan == nan)

tests/functional/verification/float_ieee32/test_float.py

@@ -12,49 +12,26 @@ def useOps(f: float, g: float) -> float:
     d = f >= g
     e = f < g
     e2 = f <= g
+    asd = 1 / 2
     return f
 
+def specialVals() -> None:
+    nan = float("nan")
+    nf = float("inF")
+    one = float("1.0")
+    Assert(nf > one)
+    Assert(not nan == nan)
+    #:: ExpectedOutput(assert.failed:assertion.false)
+    Assert(nan == nan)
+
 
 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:
+def divSave(f: float, g: float) -> None:
     #:: ExpectedOutput(application.precondition:assertion.false)
-    return f / g
+    tmp = f / g
 
 def divSave2(f: float, g: float) -> float:
     Requires(g != 0.0)

tests/functional/verification/float_ieee32/test_float_long.py

@@ -0,0 +1,64 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+#:: IgnoreFile(158)
+# Ignore this file because it non-deterministically takes very long.
+
+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
+    asd = 1 / 2
+    return f
+
+def specialVals() -> None:
+    nan = float("nan")
+    nf = float("inF")
+    one = float("1.0")
+    Assert(nf > one)
+    Assert(not nan == nan)
+    #:: ExpectedOutput(assert.failed:assertion.false)
+    Assert(nan == nan)
+
+
+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)

tests/functional/verification/float_real/test_float.py

@@ -15,6 +15,14 @@ def useOps(f: float, g: float) -> float:
     return f
 
 
+def fromString() -> None:
+    one = float("1.0")
+    two = float("2.0")
+    Assert(two > one)
+    #:: ExpectedOutput(assert.failed:assertion.false)
+    Assert(two > two)
+
+
 def cmpLits() -> None:
     Assert(3.0 > 2.0)
     Assert(1.0 <= 40.0)