introduce constant for max field size

AdaCore · Jun 21, 2022 · 78c3049 · 78c3049
1 parent 3eb40f5
commit 78c3049
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 14 deletions.
diff --git a/rflx/const.py b/rflx/const.py
@@ -2,3 +2,8 @@
 
 BUILTINS_PACKAGE = ID("__BUILTINS__")
 INTERNAL_PACKAGE = ID("__INTERNAL__")
+
+# ISSUE: Componolit/RecordFlux#1077
+# size of integers is limited to 63bits
+
+MAX_FIELD_SIZE = 63
diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
@@ -84,7 +84,7 @@
     WithClause,
 )
 from rflx.common import file_name
-from rflx.const import BUILTINS_PACKAGE, INTERNAL_PACKAGE
+from rflx.const import BUILTINS_PACKAGE, INTERNAL_PACKAGE, MAX_FIELD_SIZE
 from rflx.error import Subsystem, fail, warn
 from rflx.integration import Integration
 from rflx.model import (
@@ -719,7 +719,7 @@ def _integer_functions(self, integer: Integer) -> UnitPart:
                 ),
                 *(
                     [expr.LessEqual(expr.Variable("Val"), integer.last)]
-                    if integer.last.simplified() != expr.Number(2**63 - 1)
+                    if integer.last.simplified() != expr.Number(2**MAX_FIELD_SIZE - 1)
                     else []
                 ),
             ).simplified()
@@ -760,14 +760,14 @@ def _integer_functions(self, integer: Integer) -> UnitPart:
         return UnitPart(specification)
 
     def _enumeration_functions(self, enum: Enumeration) -> UnitPart:
-        incomplete = len(enum.literals) < 2**63
+        incomplete = len(enum.literals) < 2**MAX_FIELD_SIZE
 
         specification: ty.List[Declaration] = []
 
         validation_expression = (
             (
                 Less(Variable("Val"), Pow(Number(2), enum.size.ada_expr()))
-                if enum.size.simplified() != expr.Number(63)
+                if enum.size.simplified() != expr.Number(MAX_FIELD_SIZE)
                 else TRUE
             )
             if enum.always_valid

diff --git a/rflx/model/type_.py b/rflx/model/type_.py
@@ -123,11 +123,11 @@ def __init__(self, identifier: StrID, modulus: expr.Expr, location: Location = N
         # ISSUE: Componolit/RecordFlux#1077
         # size of integers is limited to 63bits
 
-        if modulus_int > 2**63:
+        if modulus_int > 2**const.MAX_FIELD_SIZE:
             self.error.extend(
                 [
                     (
-                        f'modulus of "{self.name}" exceeds limit (2**63)',
+                        f'modulus of "{self.name}" exceeds limit (2**{const.MAX_FIELD_SIZE})',
                         Subsystem.MODEL,
                         Severity.ERROR,
                         modulus.location,
@@ -221,11 +221,11 @@ def __init__(
                 ],
             )
             return
-        if int(last_num) >= 2**63:
+        if int(last_num) >= 2**const.MAX_FIELD_SIZE:
             self.error.extend(
                 [
                     (
-                        f'last of "{self.name}" exceeds limit (2**63 - 1)',
+                        f'last of "{self.name}" exceeds limit (2**{const.MAX_FIELD_SIZE} - 1)',
                         Subsystem.MODEL,
                         Severity.ERROR,
                         self.location,
@@ -290,11 +290,11 @@ def __init__(
         # ISSUE: Componolit/RecordFlux#1077
         # size of integers is limited to 63bits
 
-        if int(size_num) > 63:
+        if int(size_num) > const.MAX_FIELD_SIZE:
             self.error.extend(
                 [
                     (
-                        f'size of "{self.name}" exceeds limit (2**63)',
+                        f'size of "{self.name}" exceeds limit (2**{const.MAX_FIELD_SIZE})',
                         Subsystem.MODEL,
                         Severity.ERROR,
                         self.location,
@@ -411,12 +411,12 @@ def __init__(
         if self.literals.values():
             min_literal_value = min(map(int, self.literals.values()))
             max_literal_value = max(map(int, self.literals.values()))
-            if min_literal_value < 0 or max_literal_value > 2**63 - 1:
+            if min_literal_value < 0 or max_literal_value > 2**const.MAX_FIELD_SIZE - 1:
                 self.error.extend(
                     [
                         (
                             f'enumeration value of "{self.name}"'
-                            " outside of permitted range (0 .. 2**63 - 1)",
+                            f" outside of permitted range (0 .. 2**{const.MAX_FIELD_SIZE} - 1)",
                             Subsystem.MODEL,
                             Severity.ERROR,
                             self.location,
@@ -438,11 +438,11 @@ def __init__(
         # ISSUE: Componolit/RecordFlux#1077
         # size of integers is limited to 63bits
 
-        if int(size_num) > 63:
+        if int(size_num) > const.MAX_FIELD_SIZE:
             self.error.extend(
                 [
                     (
-                        f'size of "{self.name}" exceeds limit (2**63)',
+                        f'size of "{self.name}" exceeds limit (2**{const.MAX_FIELD_SIZE})',
                         Subsystem.MODEL,
                         Severity.ERROR,
                         self.location,