Add support for range integer type to generator

generator.py

@@ -84,16 +84,11 @@ def definition(self):
 
 
 class Type(SparkRepresentation):
-    def __init__(self, name, type_definition):
+    def __init__(self, name):
         self.name: str = name
-        self.type_definition: str = type_definition
 
     def specification(self):
         type_declaration = ''
-        if self.type_definition:
-            type_declaration = '   type {name} is {type_definition};\n'.format(
-                name=self.name,
-                type_definition=self.type_definition)
         return '{type_declaration}   function Convert_To_{name} is new Convert_To ({name});'.format(
             name=self.name,
             type_declaration=type_declaration)
@@ -102,6 +97,44 @@ def definition(self):  # pylint: disable=no-self-use
         return ''
 
 
+class ModularType(Type):
+    def __init__(self, name: str, modulus: str) -> None:
+        super().__init__(name)
+        self.modulus = modulus
+
+    def specification(self) -> str:
+        declaration = '   type {name} is mod {modulus};\n'.format(
+            name=self.name,
+            modulus=self.modulus)
+        return '{declaration}   function Convert_To_{name} is new Convert_To_Mod ({name});'.format(
+            name=self.name,
+            declaration=declaration)
+
+    def definition(self) -> str:  # pylint: disable=no-self-use
+        return ''
+
+
+class RangeType(Type):
+    def __init__(self, name: str, first: int, last: int, size: int) -> None:
+        super().__init__(name)
+        self.first = first
+        self.last = last
+        self.size = size
+
+    def specification(self) -> str:
+        declaration = '   type {name} is range {first} .. {last} with Size => {size};\n'.format(
+            name=self.name,
+            first=self.first,
+            last=self.last,
+            size=self.size)
+        return '{declaration}   function Convert_To_{name} is new Convert_To_Int ({name});'.format(
+            name=self.name,
+            declaration=declaration)
+
+    def definition(self):  # pylint: disable=no-self-use
+        return ''
+
+
 class Function(SparkRepresentation):
     def __init__(self, name, return_type, precondition, body):
         self.name: str = name
@@ -391,7 +424,7 @@ def process_record(name, record, type_invariant, parent_name, type_sizes):
         if c.type.identifier in BUILTIN_TYPES:
             component_last += BUILTIN_TYPES[c.type.identifier]
             if c.type.identifier.startswith('U'):
-                type_ = Type(c.type.identifier, None)
+                type_ = Type(c.type.identifier)
                 if type_ not in types:
                     types += [type_]
         elif c.type.identifier in type_sizes:
@@ -463,7 +496,21 @@ def generate(self, specifications):
             type_sizes = {}
 
             for t in specification.package.types:
-                if isinstance(t.type, parser.Modular):
+                if isinstance(t.type, parser.Range):
+                    first = int(t.type.first.literal)
+                    last = int(t.type.last.literal)
+                    size = int(t.type.size.literal)
+                    if first > last:
+                        assert False, \
+                            'unsupported definition of range type: ' \
+                            'first ({}) greater than last ({})'.format(first, last)
+                    if last - first > 2**size:
+                        assert False, \
+                            'unsupported definition of range type: ' \
+                            'size ({}) too small for range ({} .. {})'.format(size, first, last)
+                    type_sizes[t.name] = size
+                    top_package.types += [RangeType(t.name, first, last, size)]
+                elif isinstance(t.type, parser.Modular):
                     literal = t.type.expression.literal
                     match = re.match(r'^2\*\*([0-9]+)$', literal)
                     if match:
@@ -476,7 +523,7 @@ def generate(self, specifications):
                             assert False, \
                                 'unsupported definition of modular type {}'.format(literal)
                     type_sizes[t.name] = size
-                    top_package.types += [Type(t.name, 'mod {}'.format(t.type.expression.literal))]
+                    top_package.types += [ModularType(t.name, t.type.expression.literal)]
                 elif isinstance(t.type, parser.Record):
                     if t.type.abstract:
                         parser_types[t.name] = t

src/types.adb

@@ -2,31 +2,41 @@ with Ada.Text_IO;
 
 package body Types is
 
-    procedure Bytes_Put (Buffer : Bytes) with
-        SPARK_Mode => Off
-    is
-        package Modular_Text_IO is new Ada.Text_IO.Modular_IO (Byte);
-        S : String (1 .. 6);
-    begin
-        for I in Natural range Buffer'First .. Buffer'Last loop
-            Modular_Text_IO.Put(To => S, Item => Buffer (I), Base => 16);
-            if S (4) = '#' then
-                Ada.Text_IO.Put ("0" & S (5) & " ");
-            else
-                Ada.Text_IO.Put (S (4 .. 5) & " ");
-            end if;
-        end loop;
-        Ada.Text_IO.New_Line;
-    end Bytes_Put;
+   procedure Bytes_Put (Buffer : Bytes) with
+     SPARK_Mode => Off
+   is
+      package Modular_Text_IO is new Ada.Text_IO.Modular_IO (Byte);
+      S : String (1 .. 6);
+   begin
+      for I in Natural range Buffer'First .. Buffer'Last loop
+         Modular_Text_IO.Put(To => S, Item => Buffer (I), Base => 16);
+         if S (4) = '#' then
+            Ada.Text_IO.Put ("0" & S (5) & " ");
+         else
+            Ada.Text_IO.Put (S (4 .. 5) & " ");
+         end if;
+      end loop;
+      Ada.Text_IO.New_Line;
+   end Bytes_Put;
 
-    function Convert_To (Buffer : Bytes) return UXX
-    is
-        Value : UXX := 0;
-    begin
-        for i in Natural range 0 .. (UXX'Size / 8) - 1 loop
-            Value := Value + UXX (Buffer (Buffer'Last - i)) * UXX (256**i);
-        end loop;
-        return Value;
-    end Convert_To;
+   function Convert_To_Mod (Buffer : Bytes) return UXX
+   is
+      Value : UXX := 0;
+   begin
+      for i in Natural range 0 .. (UXX'Size / 8) - 1 loop
+         Value := Value + UXX (Buffer (Buffer'Last - i)) * UXX (256**i);
+      end loop;
+      return Value;
+   end Convert_To_Mod;
+
+   function Convert_To_Int (Buffer : Bytes) return Int
+   is
+      Value : Int := 0;
+   begin
+      for i in Natural range 0 .. (Int'Size / 8) - 1 loop
+         Value := Value + Int (Buffer (Buffer'Last - i)) * Int (256**i);
+      end loop;
+      return Value;
+   end Convert_To_Int;
 
 end Types;

src/types.ads

@@ -1,15 +1,21 @@
 package Types is
 
-    type Byte is mod 2**8;
-    type Bytes is array (Positive range <>) of Byte;
-    type Payload_Type is new Bytes;
+   type Byte is mod 2**8;
+   type Bytes is array (Positive range <>) of Byte;
+   type Payload_Type is new Bytes;
 
-    procedure Bytes_Put (Buffer : Bytes);
+   procedure Bytes_Put (Buffer : Bytes);
 
-    generic
-        type UXX is mod <>;
-    function Convert_To (Buffer : Bytes) return UXX with
-        Depends => (Convert_To'Result => Buffer),
+   generic
+      type UXX is mod <>;
+   function Convert_To_Mod (Buffer : Bytes) return UXX
+     with
         Pre => UXX'Size rem 8 = 0 and then Buffer'Length = UXX'Size / 8;
 
+   generic
+      type Int is range <>;
+   function Convert_To_Int (Buffer : Bytes) return Int
+     with
+       Pre => Int'Size rem 8 = 0 and then Buffer'Length = Int'Size / 8;
+
 end Types;

tests/ethernet.ads

@@ -3,9 +3,9 @@ with Types; use Types;
 package Ethernet is
 
    type U16 is mod 2**16;
-   function Convert_To_U16 is new Convert_To (U16);
+   function Convert_To_U16 is new Convert_To_Mod (U16);
 
    type U48 is mod 2**48;
-   function Convert_To_U48 is new Convert_To (U48);
+   function Convert_To_U48 is new Convert_To_Mod (U48);
 
 end Ethernet;

tests/simple_ethernet.ads

@@ -3,9 +3,9 @@ with Types; use Types;
 package Simple_Ethernet is
 
    type U16 is mod 2**16;
-   function Convert_To_U16 is new Convert_To (U16);
+   function Convert_To_U16 is new Convert_To_Mod (U16);
 
    type U48 is mod 2**48;
-   function Convert_To_U48 is new Convert_To (U48);
+   function Convert_To_U48 is new Convert_To_Mod (U48);
 
 end Simple_Ethernet;