aboutsummaryrefslogtreecommitdiffstats
path: root/src/psl/psl-nodes.adb.in
diff options
context:
space:
mode:
Diffstat (limited to 'src/psl/psl-nodes.adb.in')
-rw-r--r--src/psl/psl-nodes.adb.in388
1 files changed, 388 insertions, 0 deletions
diff --git a/src/psl/psl-nodes.adb.in b/src/psl/psl-nodes.adb.in
new file mode 100644
index 000000000..775e1d911
--- /dev/null
+++ b/src/psl/psl-nodes.adb.in
@@ -0,0 +1,388 @@
+-- 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;
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-13 07:39:43 +0000