Format big numbers with power of two

Ref. None
AdaCore · Jul 31, 2024 · 072ee01 · 072ee01
1 parent 9ef7278
commit 072ee01
Show file tree

Hide file tree

Showing 6 changed files with 54 additions and 12 deletions.
diff --git a/librapidflux/src/ty.rs b/librapidflux/src/ty.rs
@@ -42,11 +42,32 @@ impl Bounds {
             upper: self.upper.max(bounds.upper),
         }
     }
+
+    fn write_with_exponent(f: &mut impl std::fmt::Write, number: i128) -> std::fmt::Result {
+        if number > u16::MAX.into() {
+            let bits: u32 = i128::BITS - number.leading_zeros();
+            let remaining = 2i128.checked_pow(bits).unwrap_or(i128::MAX) - number;
+            debug_assert_eq!(
+                2i128.checked_pow(bits).unwrap_or(i128::MAX) - remaining,
+                number
+            );
+
+            if remaining > 0 {
+                write!(f, "2**{bits} - {remaining}")
+            } else {
+                write!(f, "2**{bits}")
+            }
+        } else {
+            write!(f, "{number}")
+        }
+    }
 }
 
 impl Display for Bounds {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        write!(f, "{} .. {}", self.lower, self.upper)
+        Self::write_with_exponent(f, self.lower)?;
+        write!(f, " .. ")?;
+        Self::write_with_exponent(f, self.upper)
     }
 }
 
@@ -122,8 +143,21 @@ mod tests {
         assert_eq!(bounds, deserialized_bounds);
     }
 
-    #[test]
-    fn test_bounds_display() {
-        assert_eq!(Bounds::new(1, 2).to_string(), "1 .. 2");
+    #[rstest]
+    #[case::small_bound(Bounds::new(1, 2), "1 .. 2")]
+    #[case::limit_bounds(
+            Bounds::new((u64::MAX - 16).into(), (u64::MAX - 1).into()),
+            "2**64 - 17 .. 2**64 - 2"
+        )
+    ]
+    #[case::limit_upper_bound(
+            Bounds::new(0, (u64::MAX - 1).into()),
+            "0 .. 2**64 - 2"
+        )
+    ]
+    #[case::bound_close_to_max_value(Bounds::new(0, i128::MAX - 1), "0 .. 2**127 - 1")]
+    #[case::upper_bound_i128_max_value(Bounds::new(0, i128::MAX), "0 .. 2**127")]
+    fn test_bounds_display(#[case] bound: Bounds, #[case] expected: &str) {
+        assert_eq!(bound.to_string(), expected);
     }
 }
diff --git a/tests/integration/specification_model_test.py b/tests/integration/specification_model_test.py
@@ -2054,7 +2054,7 @@ def test_opaque_field_size_is_aggregate(tmp_path: Path, capfd: pytest.CaptureFix
             info: Verifying __BUILTINS__::Boolean
             info: Verifying __INTERNAL__::Opaque
             info: Verifying Test::M
-            error: expected integer type "__BUILTINS__::Base_Integer" (0 .. 9223372036854775807)
+            error: expected integer type "__BUILTINS__::Base_Integer" (0 .. 2**63 - 1)
              --> {tmp_file}:5:26
               |
             5 |             with Size => [1, 2, 3];

diff --git a/tests/unit/generator/session_test.py b/tests/unit/generator/session_test.py
@@ -1204,7 +1204,7 @@ def _update_str(self) -> None:
                 ),
             ),
             RecordFluxError,
-            r"Last with type universal integer \(0 .. 9223372036854775807\) as value of message"
+            r"Last with type universal integer \(0 .. 2\*\*63 - 1\) as value of message"
             r" field not yet supported",
         ),
         (

diff --git a/tests/unit/model/message_test.py b/tests/unit/model/message_test.py
@@ -1320,7 +1320,7 @@ def test_field_size_is_aggregate() -> None:
         structure,
         types,
         r'^<stdin>:3:4: error: expected integer type "__BUILTINS__::Base_Integer" '
-        r"\(0 .. 9223372036854775807\)\n"
+        r"\(0 .. 2\*\*63 - 1\)\n"
         r"<stdin>:3:4: error: found aggregate with element type universal integer \(1 .. 2\)\n"
         r'<stdin>:1:1: note: on path "F"$',
     )

diff --git a/tests/unit/rapidflux/ty_test.py b/tests/unit/rapidflux/ty_test.py
@@ -30,9 +30,17 @@ def test_bounds_error() -> None:
         Bounds(1, 0)
 
 
-def test_bounds_str() -> None:
-    assert str(Bounds(1, 1)) == "1 .. 1"
-    assert str(Bounds(1, 100)) == "1 .. 100"
+@pytest.mark.parametrize(
+    ("bound", "expected"),
+    [
+        (Bounds(1, 1), "1 .. 1"),
+        (Bounds(1, 100), "1 .. 100"),
+        (Bounds(1, 2**64 - 1), "1 .. 2**64 - 1"),
+        (Bounds(2**32 - 1, 2**64 - 1), "2**32 - 1 .. 2**64 - 1"),
+    ],
+)
+def test_bounds_str(bound: Bounds, expected: str) -> None:
+    assert str(bound) == expected
 
 
 def test_bounds_pickle(tmp_path: Path) -> None:

diff --git a/tests/unit/typing__test.py b/tests/unit/typing__test.py
@@ -636,7 +636,7 @@ def test_check_type(actual: Type, expected: Type) -> None:
             r"^"
             r'<stdin>:10:20: error: expected message type "A"\n'
             r'<stdin>:10:20: error: found integer type "__BUILTINS__::Base_Integer"'
-            r" \(0 \.\. 9223372036854775807\)"
+            r" \(0 \.\. 2\*\*63 - 1\)"
             r"$",
         ),
         (
@@ -682,7 +682,7 @@ def test_check_type_instance(
             r"^"
             r"<stdin>:10:20: error: expected sequence type or message type\n"
             r'<stdin>:10:20: error: found integer type "__BUILTINS__::Base_Integer"'
-            r" \(0 \.\. 9223372036854775807\)"
+            r" \(0 \.\. 2\*\*63 - 1\)"
             r"$",
         ),
         (