]> git.ipfire.org Git - thirdparty/gcc.git/commitdiff
[Ada] Info. gathering in preparation for more efficiency improvements
authorBob Duff <duff@adacore.com>
Mon, 9 Aug 2021 23:06:18 +0000 (19:06 -0400)
committerPierre-Marie de Rodat <derodat@adacore.com>
Fri, 1 Oct 2021 06:13:36 +0000 (06:13 +0000)
gcc/ada/

* atree.adb: Gather and print statistics about frequency of
getter and setter calls.
* atree.ads (Print_Statistics): New procedure for printing
statistics.
* debug.adb: Document -gnatd.A switch.
* gen_il-gen.adb: Generate code for statistics gathering.
Choose the offset of Homonym early.  Misc cleanup.  Put more
comments in the generated code.
* gen_il-internals.ads (Unknown_Offset): New value to indicate
that the offset has not yet been chosen.
* gnat1drv.adb: Call Print_Statistics.
* libgnat/s-imglli.ads: Minor comment fix.
* output.ads (Write_Int_64): New procedure to write a 64-bit
value.  Needed for new statistics, and could come in handy
elsewhere.
* output.adb (Write_Int_64): Likewise.
* sinfo.ads: Remove obsolete comment. The xtreeprs program no
longer exists.
* types.ads: New 64-bit types needed for new statistics.

gcc/ada/atree.adb
gcc/ada/atree.ads
gcc/ada/debug.adb
gcc/ada/gen_il-gen.adb
gcc/ada/gen_il-internals.ads
gcc/ada/gnat1drv.adb
gcc/ada/libgnat/s-imglli.ads
gcc/ada/output.adb
gcc/ada/output.ads
gcc/ada/sinfo.ads
gcc/ada/types.ads

index e7fa8e05c3f95bb3c708bad2b6997d79e89eec05..5af4b13bb3d13896541af63021755b07c7f1f1ae 100644 (file)
@@ -211,6 +211,10 @@ package body Atree is
      (Old_N : Entity_Id; New_Kind : Entity_Kind);
    --  Above are the same as the ones for nodes, but for entities
 
+   procedure Update_Kind_Statistics (Field : Node_Or_Entity_Field);
+   --  Increment Set_Count (Field). This is in a procedure so we can put it in
+   --  pragma Debug for efficiency.
+
    procedure Init_Nkind (N : Node_Id; Val : Node_Kind);
    --  Initialize the Nkind field, which must not have been set already. This
    --  cannot be used to modify an already-initialized Nkind field. See also
@@ -905,7 +909,7 @@ package body Atree is
       Old_Kind : constant Node_Kind := Nkind (Old_N);
 
       --  If this fails, it means you need to call Reinit_Field_To_Zero before
-      --  calling Set_Nkind.
+      --  calling Mutate_Nkind.
 
    begin
       for J in Node_Field_Table (Old_Kind)'Range loop
@@ -970,11 +974,17 @@ package body Atree is
    Nkind_Offset : constant Field_Offset :=
      Field_Descriptors (F_Nkind).Offset;
 
+   procedure Update_Kind_Statistics (Field : Node_Or_Entity_Field) is
+   begin
+      Set_Count (Field) := Set_Count (Field) + 1;
+   end Update_Kind_Statistics;
+
    procedure Set_Node_Kind_Type is new Set_8_Bit_Field (Node_Kind) with Inline;
 
    procedure Init_Nkind (N : Node_Id; Val : Node_Kind) is
       pragma Assert (Field_Is_Initial_Zero (N, F_Nkind));
    begin
+      pragma Debug (Update_Kind_Statistics (F_Nkind));
       Set_Node_Kind_Type (N, Nkind_Offset, Val);
    end Init_Nkind;
 
@@ -1017,6 +1027,7 @@ package body Atree is
          Zero_Dynamic_Slots (Off_F (N) + Old_Size, Slots.Last);
       end if;
 
+      pragma Debug (Update_Kind_Statistics (F_Nkind));
       Set_Node_Kind_Type (N, Nkind_Offset, Val);
       pragma Debug (Validate_Node_Write (N));
 
@@ -1049,6 +1060,7 @@ package body Atree is
       --  For now, we are allocating all entities with the same size, so we
       --  don't need to reallocate slots here.
 
+      pragma Debug (Update_Kind_Statistics (F_Ekind));
       Set_Entity_Kind_Type (N, Ekind_Offset, Val);
       pragma Debug (Validate_Node_Write (N));
 
@@ -1535,8 +1547,7 @@ package body Atree is
       for J in Fields'Range loop
          declare
             use Seinfo;
-            Desc : Field_Descriptor renames
-              Field_Descriptors (Fields (J));
+            Desc : Field_Descriptor renames Field_Descriptors (Fields (J));
          begin
             if Desc.Kind in Node_Id_Field | List_Id_Field then
                Fix_Parent (Get_Node_Field_Union (Fix_Node, Desc.Offset));
@@ -2477,4 +2488,60 @@ package body Atree is
       Zero_Header_Slots (N);
    end Zero_Slots;
 
+   ----------------------
+   -- Print_Statistics --
+   ----------------------
+
+   procedure Print_Statistics is
+      Total, G_Total, S_Total : Call_Count := 0;
+   begin
+      Write_Line ("Frequency of field getter and setter calls:");
+
+      for Field in Node_Or_Entity_Field loop
+         G_Total := G_Total + Get_Count (Field);
+         S_Total := S_Total + Set_Count (Field);
+         Total := G_Total + S_Total;
+      end loop;
+
+      Write_Int_64 (Total);
+      Write_Str (" (100%) = ");
+      Write_Int_64 (G_Total);
+      Write_Str (" + ");
+      Write_Int_64 (S_Total);
+      Write_Line (" total getter and setter calls");
+
+      for Field in Node_Or_Entity_Field loop
+         declare
+            G : constant Call_Count := Get_Count (Field);
+            S : constant Call_Count := Set_Count (Field);
+            GS : constant Call_Count := G + S;
+
+            Percent : constant Int :=
+              Int ((Long_Float (GS) / Long_Float (Total)) * 100.0);
+
+            use Seinfo;
+            Desc : Field_Descriptor renames Field_Descriptors (Field);
+            Slot : constant Field_Offset :=
+              (Field_Size (Desc.Kind) * Desc.Offset) / Slot_Size;
+
+         begin
+            Write_Int_64 (GS);
+            Write_Str (" (");
+            Write_Int (Percent);
+            Write_Str ("%)");
+            Write_Str (" = ");
+            Write_Int_64 (G);
+            Write_Str (" + ");
+            Write_Int_64 (S);
+            Write_Str (" ");
+            Write_Str (Node_Or_Entity_Field'Image (Field));
+            Write_Str (" in slot ");
+            Write_Int (Int (Slot));
+            Write_Str (" size ");
+            Write_Int (Int (Field_Size (Desc.Kind)));
+            Write_Eol;
+         end;
+      end loop;
+   end Print_Statistics;
+
 end Atree;
index 8836bb84e1accb98fbd2a742ef79a8c9bd6cefad..7120ecf3f807fc4587ce33ecc9c412d6790c9839 100644 (file)
@@ -862,4 +862,14 @@ package Atree is
 
    end Atree_Private_Part;
 
+   --  Statistics:
+
+   subtype Call_Count is Nat_64;
+   Get_Count, Set_Count : array (Node_Or_Entity_Field) of Call_Count :=
+     (others => 0);
+   --  Number of calls to each getter and setter. See documentaton for
+   --  -gnatd.A.
+
+   procedure Print_Statistics;
+
 end Atree;
index 5245feb3b27bdcc35d0aeb71cd1708a5dc9478e3..a7cdfae25819b863a9aeedc4f50e62aa57851422 100644 (file)
@@ -112,7 +112,7 @@ package body Debug is
    --  d.y  Disable implicit pragma Elaborate_All on task bodies
    --  d.z  Restore previous support for frontend handling of Inline_Always
 
-   --  d.A
+   --  d.A  Enable statistics printing in Atree
    --  d.B  Generate a bug box on abort_statement
    --  d.C  Generate concatenation call, do not generate inline code
    --  d.D  Disable errors on use of overriding keyword in Ada 95 mode
@@ -830,6 +830,10 @@ package body Debug is
    --       handling of Inline_Always by the front end on such targets. For the
    --       targets that do not use the GCC back end, this switch is ignored.
 
+   --  d.A  Enable statistics printing in Atree. First set Statistics_Enabled
+   --       in gen_il-gen.adb to True, then rebuild, then run the compiler with
+   --       -gnatd.A. You might want to apply "sort -nr" to the output.
+
    --  d.B  Generate a bug box when we see an abort_statement, even though
    --       there is no bug. Useful for testing Comperr.Compiler_Abort: write
    --       some code containing an abort_statement, and compile it with
index 2fbec00e5486557fa90e97c34aa390a05e0ee3cc..dd1e3a158448a0332a37215df5ee1a5738197e18 100644 (file)
@@ -28,11 +28,18 @@ with Ada.Text_IO;
 
 package body Gen_IL.Gen is
 
+   Statistics_Enabled : constant Boolean := False;
+   --  Change to True or False to enable/disable statistics printed by
+   --  Atree. Should normally be False, for efficiency. Also compile with
+   --  -gnatd.A to get the statistics printed.  Enabling these statistics
+   --  makes the compiler about 20% slower.
+
    Num_Header_Slots : constant := 3;
    --  Number of header slots; the first Num_Header_Slots slots are stored in
    --  the header; the rest are dynamically allocated in the Slots table. We
    --  need to subtract this off when accessing dynamic slots. The constant
-   --  Seinfo.N_Head will contain this value.
+   --  Seinfo.N_Head will contain this value. Fields that are allocated in the
+   --  header slots are quicker to access.
    --
    --  This number can be adjusted for efficiency. We choose 3 because the
    --  minimum node size is 3 slots, and because that causes the size of type
@@ -326,7 +333,7 @@ package body Gen_IL.Gen is
             Pre => new String'(Pre),
             Pre_Get => new String'(Pre_Get),
             Pre_Set => new String'(Pre_Set),
-            Offset => <>); -- filled in later
+            Offset => Unknown_Offset);
 
       --  The Field_Table entry has already been created by the 'then' part
       --  above. Now we're seeing the same field being "created" again in a
@@ -938,8 +945,7 @@ package body Gen_IL.Gen is
            (F : Field_Enum; Offset : Field_Offset);
          --  Mark the offset as "in use"
 
-         function Choose_Offset
-           (F : Field_Enum) return Field_Offset;
+         procedure Choose_Offset (F : Field_Enum);
          --  Choose an offset for this field
 
          function Offset_OK
@@ -979,14 +985,14 @@ package body Gen_IL.Gen is
             end loop;
          end Set_Offset_In_Use;
 
-         function Choose_Offset
-           (F : Field_Enum) return Field_Offset is
+         procedure Choose_Offset (F : Field_Enum) is
          begin
             for Offset in Field_Offset loop
                if Offset_OK (F, Offset) then
                   Set_Offset_In_Use (F, Offset);
 
-                  return Offset;
+                  Field_Table (F).Offset := Offset;
+                  return;
                end if;
             end loop;
 
@@ -1059,8 +1065,18 @@ package body Gen_IL.Gen is
          --  complication compared to standard graph coloring is that fields
          --  are different sizes.
 
+         --  First choose offsets for some heavily-used fields, so they will
+         --  get low offsets, so they will wind up in the node header for
+         --  faster access.
+
+         Choose_Offset (Homonym);
+
+         --  Then loop through them all, skipping the ones we did above
+
          for F of All_Fields loop
-            Field_Table (F).Offset := Choose_Offset (F);
+            if Field_Table (F).Offset = Unknown_Offset then
+               Choose_Offset (F);
+            end if;
          end loop;
 
       end Compute_Field_Offsets;
@@ -1611,14 +1627,6 @@ package body Gen_IL.Gen is
          Put (S, LF & "subtype Flag is Boolean;" & LF & LF);
       end Put_Type_And_Subtypes;
 
-      function Low_Level_Getter_Name (T : Type_Enum) return String is
-        ("Get_" & Image (T));
-      function Low_Level_Setter_Name (T : Type_Enum) return String is
-        ("Set_" & Image (T));
-      function Low_Level_Setter_Name (F : Field_Enum) return String is
-        (Low_Level_Setter_Name (Field_Table (F).Field_Type) &
-           (if Setter_Needs_Parent (F) then "_With_Parent" else ""));
-
       -------------------------------------------
       -- Put_Casts --
       -------------------------------------------
@@ -1705,6 +1713,25 @@ package body Gen_IL.Gen is
       --  Node_Id or Entity_Id, and the getter and setter will have
       --  preconditions.
 
+      procedure Put_Get_Set_Incr
+        (S : in out Sink; F : Field_Enum; Get_Or_Set : String)
+        with Pre => Get_Or_Set in "Get" | "Set";
+      --  If statistics are enabled, put the appropriate increment statement
+
+      ----------------------
+      -- Put_Get_Set_Incr --
+      ----------------------
+
+      procedure Put_Get_Set_Incr
+        (S : in out Sink; F : Field_Enum; Get_Or_Set : String) is
+      begin
+         if Statistics_Enabled then
+            Put (S, "Atree." & Get_Or_Set & "_Count (" & F_Image (F) &
+                   ") := Atree." & Get_Or_Set & "_Count (" &
+                   F_Image (F) & ") + 1;" & LF);
+         end if;
+      end Put_Get_Set_Incr;
+
       ------------------------
       -- Node_To_Fetch_From --
       ------------------------
@@ -1831,7 +1858,8 @@ package body Gen_IL.Gen is
             pragma Assert (Field_Size (Rec.Field_Type) = 32);
             Put (S, LF);
             Increase_Indent (S, 2);
-            Put (S, "(if Raw = 0 then " & Special_Default (Rec.Field_Type) & " else " & "Cast (Raw));");
+            Put (S, "(if Raw = 0 then " & Special_Default (Rec.Field_Type) &
+                   " else " & "Cast (Raw));");
             Decrease_Indent (S, 2);
 
          else
@@ -1856,6 +1884,7 @@ package body Gen_IL.Gen is
             Put (S, "pragma Assert (" & Rec.Pre_Get.all & ");" & LF);
          end if;
 
+         Put_Get_Set_Incr (S, F, "Get");
          Put (S, "return Val;" & LF);
          Decrease_Indent (S, 3);
          Put (S, "end " & Image (F) & ";" & LF & LF);
@@ -1954,6 +1983,7 @@ package body Gen_IL.Gen is
             Put (S, "S := Slot (Raw);" & LF);
          end if;
 
+         Put_Get_Set_Incr (S, F, "Set");
          Decrease_Indent (S, 3);
          Put (S, "end Set_" & Image (F) & ";" & LF & LF);
       end Put_Setter_Body;
@@ -2310,6 +2340,40 @@ package body Gen_IL.Gen is
          if Root = Node_Kind then
             declare
                First_Time : Boolean := True;
+               FS, FB, LB : Bit_Offset;
+               --  Field size in bits, first bit, and last bit for the previous
+               --  time around the loop. Used to print a comment after ",".
+
+               procedure One_Comp (F : Field_Enum);
+
+               procedure One_Comp (F : Field_Enum) is
+                  Offset : constant Field_Offset :=  Field_Table (F).Offset;
+               begin
+                  if First_Time then
+                     First_Time := False;
+                  else
+                     Put (S, ",");
+
+                     --  Print comment showing field's bits, except for 1-bit
+                     --  fields.
+
+                     if FS /= 1 then
+                        Put (S, " -- *" & Image (FS) & " = bits " &
+                               Image (FB) & ".." & Image (LB));
+                     end if;
+
+                     Put (S, LF);
+                  end if;
+
+                  Put (S, F_Image (F) & " => (" &
+                       Image (Field_Table (F).Field_Type) & "_Field, " &
+                       Image (Offset) & ")");
+
+                  FS := Field_Size (F);
+                  FB := First_Bit (F, Offset);
+                  LB := Last_Bit (F, Offset);
+               end One_Comp;
+
             begin
                Put (S, LF & "--  Table mapping fields to kind and offset:" & LF & LF);
 
@@ -2321,22 +2385,11 @@ package body Gen_IL.Gen is
                Increase_Indent (S, 1);
 
                for F in Node_Field loop
-                  if First_Time then
-                     First_Time := False;
-                  else
-                     Put (S, "," & LF);
-                  end if;
-
-                  Put (S, F_Image (F) & " => (" &
-                       Image (Field_Table (F).Field_Type) & "_Field, " &
-                       Image (Field_Table (F).Offset) & ")");
+                  One_Comp (F);
                end loop;
 
                for F in Entity_Field loop
-                  Put (S, "," & LF);
-                  Put (S, F_Image (F) & " => (" &
-                       Image (Field_Table (F).Field_Type) & "_Field, " &
-                       Image (Field_Table (F).Offset) & ")");
+                  One_Comp (F);
                end loop;
 
                Decrease_Indent (S, 1);
@@ -2420,8 +2473,8 @@ package body Gen_IL.Gen is
          --  the base type, because we are using zero-origin addressing in
          --  Atree.
 
-         Put (S, "N_Head : constant Field_Offset := " & N_Head & ";" & LF);
          Put (S, "" & LF);
+         Put (S, "N_Head : constant Field_Offset := " & N_Head & ";" & LF);
          Put (S, "type Node_Header_Slots is" & LF);
          Put (S, "  array (Field_Offset range 0 .. N_Head - 1) of aliased Slot;" & LF);
          Put (S, "type Node_Header is record" & LF);
@@ -2956,6 +3009,7 @@ package body Gen_IL.Gen is
 
          declare
             First_Time : Boolean := True;
+
          begin
             for T in Concrete_Type loop
                if First_Time then
@@ -2977,40 +3031,45 @@ package body Gen_IL.Gen is
                declare
                   First_Time : Boolean := True;
                   First_Bit : Bit_Offset := 0;
+                  F : Opt_Field_Enum;
+
+                  function Node_Field_Of_Entity return String is
+                     (if T in Entity_Type and then F in Node_Field then
+                       " -- N" else "");
+                  --  A comment to put out for fields of entities that are
+                  --  shared with nodes, such as Chars.
+
                begin
                   while First_Bit < Type_Bit_Size_Aligned (T) loop
                      if First_Time then
                         First_Time := False;
                      else
-                        Put (B, "," & LF);
+                        Put (B, "," & Node_Field_Of_Entity & LF);
                      end if;
 
+                     F := Type_Layout (T) (First_Bit);
+
                      declare
-                        F : constant Opt_Field_Enum :=
-                          Type_Layout (T) (First_Bit);
+                        Last_Bit : constant Bit_Offset :=
+                          Get_Last_Bit (T, F, First_Bit);
                      begin
-                        declare
-                           Last_Bit : constant Bit_Offset :=
-                             Get_Last_Bit (T, F, First_Bit);
-                        begin
+                        pragma Assert
+                          (Type_Layout (T) (First_Bit .. Last_Bit) =
+                                           (First_Bit .. Last_Bit => F));
+
+                        if Last_Bit = First_Bit then
+                           Put (B, First_Bit_Image (First_Bit) & " => " &
+                                Image_Or_Waste (F));
+                        else
                            pragma Assert
-                             (Type_Layout (T) (First_Bit .. Last_Bit) =
-                                              (First_Bit .. Last_Bit => F));
-
-                           if Last_Bit = First_Bit then
-                              Put (B, First_Bit_Image (First_Bit) & " => " &
-                                   Image_Or_Waste (F));
-                           else
-                              pragma Assert
-                                (if F /= No_Field then
-                                  First_Bit mod Field_Size (F) = 0);
-                              Put (B, First_Bit_Image (First_Bit) & " .. " &
-                                   Last_Bit_Image (Last_Bit) & " => " &
-                                   Image_Or_Waste (F));
-                           end if;
-
-                           First_Bit := Last_Bit + 1;
-                        end;
+                             (if F /= No_Field then
+                               First_Bit mod Field_Size (F) = 0);
+                           Put (B, First_Bit_Image (First_Bit) & " .. " &
+                                Last_Bit_Image (Last_Bit) & " => " &
+                                Image_Or_Waste (F));
+                        end if;
+
+                        First_Bit := Last_Bit + 1;
                      end;
                   end loop;
                end;
index 53c23a278518f84f95830df5f7ed193ebcb7f22d..11a99123f67db769b89a43b35d41e034f3dca661 100644 (file)
@@ -147,6 +147,9 @@ package Gen_IL.Internals is
    --  The default is No_Type_Only, indicating the field is not one of
    --  these special "[... only]" ones.
 
+   Unknown_Offset : constant := -1;
+   --  Initial value of Offset, so we can tell whether it has been set
+
    type Field_Info is record
       Have_This_Field : Type_Vector;
       --  Types that have this field
@@ -162,7 +165,7 @@ package Gen_IL.Internals is
       --  Above record the information in the calls to Create_...Field.
       --  See Gen_IL.Gen for details.
 
-      Offset          : Field_Offset;
+      Offset : Field_Offset'Base range Unknown_Offset .. Field_Offset'Last;
       --  Offset of the field from the start of the node, in units of the field
       --  size. So if a field is 4 bits in size, it starts at bit number
       --  Offset*4 from the start of the node.
index 95c1537c4847808e3cdbffdfd4734d5fa8b32bfe..55f9efa777bc6b1b2c8dee9b787382f019e1603b 100644 (file)
@@ -1695,6 +1695,10 @@ begin
 
    <<End_Of_Program>>
 
+   if Debug_Flag_Dot_AA then
+      Atree.Print_Statistics;
+   end if;
+
 --  The outer exception handler handles an unrecoverable error
 
 exception
index 2e0b42c4dca68e1c9e12ed8474b6560492d65a6d..e6e3efccd64d9162b24b71b79c422131c01d3382 100644 (file)
@@ -30,8 +30,8 @@
 ------------------------------------------------------------------------------
 
 --  This package contains the routines for supporting the Image attribute for
---  signed integer types larger Integer, and also for conversion operations
---  required in Text_IO.Integer_IO for such types.
+--  signed integer types larger than Integer, and also for conversion
+--  operations required in Text_IO.Integer_IO for such types.
 
 with System.Image_I;
 
index e886b92b7b704c877a81ddc5a1d2d4786fc5fc78..00202fd1d2d8a4d875a469c45bef982b9248aeb1 100644 (file)
@@ -467,6 +467,32 @@ package body Output is
       end if;
    end Write_Int;
 
+   ------------------
+   -- Write_Int_64 --
+   ------------------
+
+   procedure Write_Int_64 (Val : Int_64) is
+      subtype Nonpositive is Int_64 range Int_64'First .. 0;
+      procedure Write_Abs (Val : Nonpositive);
+
+      procedure Write_Abs (Val : Nonpositive) is
+      begin
+         if Val < -9 then
+            Write_Abs (Val / 10);
+         end if;
+
+         Write_Char (Character'Val (-(Val rem 10) + Character'Pos ('0')));
+      end Write_Abs;
+
+   begin
+      if Val < 0 then
+         Write_Char ('-');
+         Write_Abs (Val);
+      else
+         Write_Abs (-Val);
+      end if;
+   end Write_Int_64;
+
    ----------------
    -- Write_Line --
    ----------------
index 6a36533fde4f175edbbb5e15815f1a7db97c9a4f..5058d6dfbe1757cc15fb2456489d5d91a73d887d 100644 (file)
@@ -124,6 +124,7 @@ package Output is
    --  Similar as Write_Eol, except that trailing spaces are not removed
 
    procedure Write_Int (Val : Int);
+   procedure Write_Int_64 (Val : Int_64);
    --  Write an integer value with no leading blanks or zeroes. Negative values
    --  are preceded by a minus sign).
 
index 20a61251a9d6c3656cdcbc19ed15189c62211fcf..b99edf75891e6b7356ff47de2c303f06addfac2a 100644 (file)
@@ -411,10 +411,6 @@ package Sinfo is
    --       Assignment_OK             set if modification is OK
    --       Is_Controlling_Actual     set for controlling argument
 
-   --  Note: the utility program that creates the Treeprs spec (in the file
-   --  xtreeprs.adb) knows about the special fields here, so it must be
-   --  modified if any change is made to these fields.
-
    --  Note: see under (EXPRESSION) for further details on the use of
    --  the Paren_Count field to record the number of parentheses levels.
 
index 07b0960c1777b5953c154ed102fa9aca9368d9e7..32194e8e75fd2d32db183bf1ca80b29ff5ce685d 100644 (file)
@@ -61,6 +61,13 @@ package Types is
 
    subtype Nonzero_Int is Int with Predicate => Nonzero_Int /= 0;
 
+   type Int_64 is range -2 ** 63 .. +2 ** 63 - 1;
+   --  Signed 64-bit integer
+
+   subtype Nat_64 is Int_64 range 0 .. Int_64'Last;
+   subtype Pos_64 is Int_64 range 1 .. Int_64'Last;
+   subtype Nonzero_Int_64 is Int_64 with Predicate => Nonzero_Int_64 /= 0;
+
    type Word is mod 2 ** 32;
    --  Unsigned 32-bit integer