path: root/src/psl/psl-nodes.adb.in

--  This is in fact -*- Ada -*-
with Ada.Unchecked_Conversion;
with GNAT.Table;
with PSL.Errors;
with PSL.Hash;
with PSL.Nodes_Meta; use PSL.Nodes_Meta;

package body PSL.Nodes is
   --  Suppress the access check of the table base.  This is really safe to
   --  suppress this check because the table base cannot be null.
   pragma Suppress (Access_Check);

   --  Suppress the index check on the table.
   --  Could be done during non-debug, since this may catch errors (reading
   --  Null_Node.
   --pragma Suppress (Index_Check);

   type Format_Type is
     (
      Format_Short
     );

   -- Common fields are:
   --   Flag1 : Boolean
   --   Flag2 : Boolean
   --   Flag3 : Boolean
   --   Flag4 : Boolean
   --   Flag5 : Boolean
   --   Flag6 : Boolean
   --   Nkind : Kind_Type
   --   State1 : Bit2_Type
   --   State2 : Bit2_Type
   --   Location : Int32
   --   Field1 : Node
   --   Field2 : Node
   --   Field3 : Node
   --   Field4 : Node

   -- Fields of Format_Short:
   --   Field5 : Node
   --   Field6 : Node

   type State_Type is range 0 .. 3;
   type Bit3_Type is range 0 .. 7;

   type Node_Record is record
      Kind : Nkind;
      Flag1 : Boolean;
      Flag2 : Boolean;
      Flag3 : Boolean;
      Flag4 : Boolean;
      Flag5 : Boolean;
      Flag6 : Boolean;
      Flag7 : Boolean;
      Flag8 : Boolean;
      Flag9 : Boolean;
      Flag10 : Boolean;
      Flag11 : Boolean;
      Flag12 : Boolean;
      Flag13 : Boolean;
      Flag14 : Boolean;
      Flag15 : Boolean;
      Flag16 : Boolean;
      State1 : State_Type;
      B3_1 : Bit3_Type;
      Flag17 : Boolean;
      Flag18 : Boolean;
      Flag19 : Boolean;

      Location : Int32;
      Field1 : Node;
      Field2 : Node;
      Field3 : Node;
      Field4 : Node;
      Field5 : Node;
      Field6 : Node;
   end record;
   pragma Pack (Node_Record);
   for Node_Record'Size use 8 * 32;

   package Nodet is new GNAT.Table
     (Table_Component_Type => Node_Record,
      Table_Index_Type => Node,
      Table_Low_Bound => 1,
      Table_Initial => 1024,
      Table_Increment => 100);

   Init_Node : constant Node_Record := (Kind => N_Error,
                                        Flag1 => False,
                                        Flag2 => False,
                                        State1 => 0,
                                        B3_1 => 0,
                                        Location => 0,
                                        Field1 => 0,
                                        Field2 => 0,
                                        Field3 => 0,
                                        Field4 => 0,
                                        Field5 => 0,
                                        Field6 => 0,
                                        others => False);

   Free_Nodes : Node := Null_Node;


   function Get_Last_Node return Node is
   begin
      return Nodet.Last;
   end Get_Last_Node;

   function Node_To_Uns32 is new Ada.Unchecked_Conversion
     (Source => Node, Target => Uns32);

   function Uns32_To_Node is new Ada.Unchecked_Conversion
     (Source => Uns32, Target => Node);

   function Node_To_Int32 is new Ada.Unchecked_Conversion
     (Source => Node, Target => Int32);

   function Int32_To_Node is new Ada.Unchecked_Conversion
     (Source => Int32, Target => Node);

   function Node_To_NFA is new Ada.Unchecked_Conversion
     (Source => Node, Target => NFA);

   function NFA_To_Node is new Ada.Unchecked_Conversion
     (Source => NFA, Target => Node);

   function Node_To_HDL_Node is new Ada.Unchecked_Conversion
     (Source => Node, Target => HDL_Node);

   function HDL_Node_To_Node is new Ada.Unchecked_Conversion
     (Source => HDL_Node, Target => Node);

   procedure Set_Kind (N : Node; K : Nkind) is
   begin
      Nodet.Table (N).Kind := K;
   end Set_Kind;

   function Get_Kind (N : Node) return Nkind is
   begin
      return Nodet.Table (N).Kind;
   end Get_Kind;


   procedure Set_Flag1 (N : Node; Flag : Boolean) is
   begin
      Nodet.Table (N).Flag1 := Flag;
   end Set_Flag1;

   function Get_Flag1 (N : Node) return Boolean is
   begin
      return Nodet.Table (N).Flag1;
   end Get_Flag1;

   procedure Set_Flag2 (N : Node; Flag : Boolean) is
   begin
      Nodet.Table (N).Flag2 := Flag;
   end Set_Flag2;

   function Get_Flag2 (N : Node) return Boolean is
   begin
      return Nodet.Table (N).Flag2;
   end Get_Flag2;


   procedure Set_State1 (N : Node; S : State_Type) is
   begin
      Nodet.Table (N).State1 := S;
   end Set_State1;

   function Get_State1 (N : Node) return State_Type is
   begin
      return Nodet.Table (N).State1;
   end Get_State1;


   function Get_Location (N : Node) return Location_Type is
   begin
      return Location_Type (Nodet.Table (N).Location);
   end Get_Location;

   procedure Set_Location (N : Node; Loc : Location_Type) is
   begin
      Nodet.Table (N).Location := Int32 (Loc);
   end Set_Location;


   procedure Set_Field1 (N : Node; V : Node) is
   begin
      Nodet.Table (N).Field1 := V;
   end Set_Field1;

   function Get_Field1 (N : Node) return Node is
   begin
      return Nodet.Table (N).Field1;
   end Get_Field1;


   procedure Set_Field2 (N : Node; V : Node) is
   begin
      Nodet.Table (N).Field2 := V;
   end Set_Field2;

   function Get_Field2 (N : Node) return Node is
   begin
      return Nodet.Table (N).Field2;
   end Get_Field2;


   function Get_Field3 (N : Node) return Node is
   begin
      return Nodet.Table (N).Field3;
   end Get_Field3;

   procedure Set_Field3 (N : Node; V : Node) is
   begin
      Nodet.Table (N).Field3 := V;
   end Set_Field3;


   function Get_Field4 (N : Node) return Node is
   begin
      return Nodet.Table (N).Field4;
   end Get_Field4;

   procedure Set_Field4 (N : Node; V : Node) is
   begin
      Nodet.Table (N).Field4 := V;
   end Set_Field4;


   function Get_Field5 (N : Node) return Node is
   begin
      return Nodet.Table (N).Field5;
   end Get_Field5;

   procedure Set_Field5 (N : Node; V : Node) is
   begin
      Nodet.Table (N).Field5 := V;
   end Set_Field5;


   function Get_Field6 (N : Node) return Node is
   begin
      return Nodet.Table (N).Field6;
   end Get_Field6;

   procedure Set_Field6 (N : Node; V : Node) is
   begin
      Nodet.Table (N).Field6 := V;
   end Set_Field6;


   function Get_Format (Kind : Nkind) return Format_Type;
   pragma Unreferenced (Get_Format);

   function Create_Node (Kind : Nkind) return Node
   is
      Res : Node;
   begin
      if Free_Nodes /= Null_Node then
         Res := Free_Nodes;
         Free_Nodes := Get_Field1 (Res);
      else
         Nodet.Increment_Last;
         Res := Nodet.Last;
      end if;
      Nodet.Table (Res) := Init_Node;
      Set_Kind (Res, Kind);
      return Res;
   end Create_Node;

   procedure Free_Node (N : Node)
   is
   begin
      Set_Kind (N, N_Error);
      Set_Field1 (N, Free_Nodes);
      Free_Nodes := N;
   end Free_Node;

   procedure Failed (Msg : String; N : Node)
   is
   begin
      Errors.Error_Kind (Msg, N);
   end Failed;

   procedure Init is
   begin
      Nodet.Init;
      if Create_Node (N_False) /= False_Node then
         raise Internal_Error;
      end if;
      if Create_Node (N_True) /= True_Node then
         raise Internal_Error;
      end if;
      if Create_Node (N_Number) /= One_Node then
         raise Internal_Error;
      end if;
      Set_Value (One_Node, 1);
      if Create_Node (N_EOS) /= EOS_Node then
         raise Internal_Error;
      end if;
      Set_Hash (EOS_Node, 0);
      PSL.Hash.Init;
   end Init;

   function Get_Psl_Type (N : Node) return PSL_Types is
   begin
      case Get_Kind (N) is
         when N_And_Prop
           | N_Or_Prop
           | N_Log_Imp_Prop
           | N_Always
           | N_Never
           | N_Eventually
           | N_Next
           | N_Next_E
           | N_Next_A
           | N_Next_Event
           | N_Next_Event_A
           | N_Next_Event_E
           | N_Before
           | N_Until
           | N_Abort
           | N_Strong
           | N_Property_Parameter
           | N_Property_Instance =>
            return Type_Property;
         when N_Braced_SERE
           | N_Concat_SERE
           | N_Fusion_SERE
           | N_Within_SERE
           | N_Overlap_Imp_Seq
           | N_Imp_Seq
           | N_And_Seq
           | N_Or_Seq
           | N_Match_And_Seq
           | N_Star_Repeat_Seq
           | N_Goto_Repeat_Seq
           | N_Equal_Repeat_Seq
           | N_Plus_Repeat_Seq
           | N_Clock_Event
           | N_Sequence_Instance
           | N_Endpoint_Instance
           | N_Sequence_Parameter =>
            return Type_Sequence;
         when N_Name =>
            return Get_Psl_Type (Get_Decl (N));
         when N_HDL_Expr =>
            --  FIXME.
            return Type_Boolean;
         when N_Or_Bool
           | N_And_Bool
           | N_Not_Bool
           | N_Imp_Bool
           | N_False
           | N_True
           | N_Boolean_Parameter =>
            return Type_Boolean;
         when N_Number
           | N_Const_Parameter =>
            return Type_Numeric;
         when N_Vmode
           | N_Vunit
           | N_Vprop
           | N_Hdl_Mod_Name
           | N_Assert_Directive
           | N_Sequence_Declaration
           | N_Endpoint_Declaration
           | N_Property_Declaration
           | N_Actual
           | N_Name_Decl
           | N_Error
           | N_EOS =>
            PSL.Errors.Error_Kind ("get_psl_type", N);
      end case;
   end Get_Psl_Type;

   procedure Reference_Failed (Msg : String; N : Node) is
   begin
      Failed (Msg, N);
   end Reference_Failed;
   pragma Unreferenced (Reference_Failed);

   --  Subprograms

end PSL.Nodes;