diff options
| author | Tristan Gingold <tgingold@free.fr> | 2014-11-04 20:14:19 +0100 |
|---|---|---|
| committer | Tristan Gingold <tgingold@free.fr> | 2014-11-04 20:14:19 +0100 |
| commit | 9c195bf5d86d67ea5eb419ccf6e48dc153e57c68 (patch) | |
| tree | 575346e529b99e26382b4a06f6ff2caa0b391ab2 /src/psl | |
| parent | 184a123f91e07c927292d67462561dc84f3a920d (diff) | |
| download | ghdl-9c195bf5d86d67ea5eb419ccf6e48dc153e57c68.tar.gz ghdl-9c195bf5d86d67ea5eb419ccf6e48dc153e57c68.tar.bz2 ghdl-9c195bf5d86d67ea5eb419ccf6e48dc153e57c68.zip | |
Move sources to src/ subdirectory.
Diffstat (limited to 'src/psl')
30 files changed, 7521 insertions, 0 deletions
diff --git a/src/psl/psl-build.adb b/src/psl/psl-build.adb new file mode 100644 index 000000000..c3e47baa6 --- /dev/null +++ b/src/psl/psl-build.adb @@ -0,0 +1,1009 @@ +with GNAT.Table; +with Ada.Text_IO; use Ada.Text_IO; +with Types; use Types; +with PSL.Errors; use PSL.Errors; +with PSL.CSE; use PSL.CSE; +with PSL.QM; +with PSL.Disp_NFAs; use PSL.Disp_NFAs; +with PSL.Optimize; use PSL.Optimize; +with PSL.NFAs.Utils; +with PSL.Prints; +with PSL.NFAs; use PSL.NFAs; + +package body PSL.Build is + function Build_SERE_FA (N : Node) return NFA; + + + package Intersection is + function Build_Inter (L, R : NFA; Match_Len : Boolean) return NFA; + end Intersection; + + package body Intersection is + + type Stack_Entry_Id is new Natural; + No_Stack_Entry : constant Stack_Entry_Id := 0; + type Stack_Entry is record + L, R : NFA_State; + Res : NFA_State; + Next_Unhandled : Stack_Entry_Id; + end record; + + package Stackt is new GNAT.Table + (Table_Component_Type => Stack_Entry, + Table_Index_Type => Stack_Entry_Id, + Table_Low_Bound => 1, + Table_Initial => 128, + Table_Increment => 100); + + First_Unhandled : Stack_Entry_Id; + + procedure Init_Stack is + begin + Stackt.Init; + First_Unhandled := No_Stack_Entry; + end Init_Stack; + + function Not_Empty return Boolean is + begin + return First_Unhandled /= No_Stack_Entry; + end Not_Empty; + + procedure Pop_State (L, R : out NFA_State) is + begin + L := Stackt.Table (First_Unhandled).L; + R := Stackt.Table (First_Unhandled).R; + First_Unhandled := Stackt.Table (First_Unhandled).Next_Unhandled; + end Pop_State; + + function Get_State (N : NFA; L, R : NFA_State) return NFA_State + is + Res : NFA_State; + begin + for I in Stackt.First .. Stackt.Last loop + if Stackt.Table (I).L = L + and then Stackt.Table (I).R = R + then + return Stackt.Table (I).Res; + end if; + end loop; + Res := Add_State (N); + Stackt.Append ((L => L, R => R, Res => Res, + Next_Unhandled => First_Unhandled)); + First_Unhandled := Stackt.Last; + return Res; + end Get_State; + + function Build_Inter (L, R : NFA; Match_Len : Boolean) return NFA + is + Start_L, Start_R : NFA_State; + Final_L, Final_R : NFA_State; + S_L, S_R : NFA_State; + E_L, E_R : NFA_Edge; + Res : NFA; + Start : NFA_State; + Extra_L, Extra_R : NFA_Edge; + begin + Start_L := Get_Start_State (L); + Start_R := Get_Start_State (R); + Final_R := Get_Final_State (R); + Final_L := Get_Final_State (L); + + if False then + Disp_Body (L); + Disp_Body (R); + Put ("//start state: "); + Disp_State (Start_L); + Put (","); + Disp_State (Start_R); + New_Line; + end if; + + if Match_Len then + Extra_L := No_Edge; + Extra_R := No_Edge; + else + Extra_L := Add_Edge (Final_L, Final_L, True_Node); + Extra_R := Add_Edge (Final_R, Final_R, True_Node); + end if; + + Res := Create_NFA; + Init_Stack; + Start := Get_State (Res, Start_L, Start_R); + Set_Start_State (Res, Start); + + while Not_Empty loop + Pop_State (S_L, S_R); + + if False then + Put ("//poped state: "); + Disp_State (S_L); + Put (","); + Disp_State (S_R); + New_Line; + end if; + + E_L := Get_First_Src_Edge (S_L); + while E_L /= No_Edge loop + E_R := Get_First_Src_Edge (S_R); + while E_R /= No_Edge loop + if not (E_L = Extra_L and E_R = Extra_R) then + Add_Edge (Get_State (Res, S_L, S_R), + Get_State (Res, + Get_Edge_Dest (E_L), + Get_Edge_Dest (E_R)), + Build_Bool_And (Get_Edge_Expr (E_L), + Get_Edge_Expr (E_R))); + end if; + E_R := Get_Next_Src_Edge (E_R); + end loop; + E_L := Get_Next_Src_Edge (E_L); + end loop; + end loop; + Set_Final_State (Res, Get_State (Res, Final_L, Final_R)); + Remove_Unreachable_States (Res); + + if not Match_Len then + Remove_Edge (Extra_L); + Remove_Edge (Extra_R); + end if; + + -- FIXME: free L and R. + return Res; + end Build_Inter; + end Intersection; + + -- All edges from A are duplicated using B as a source. + -- Handle epsilon-edges. + procedure Duplicate_Src_Edges (N : NFA; A, B : NFA_State) + is + pragma Unreferenced (N); + E : NFA_Edge; + Expr : Node; + Dest : NFA_State; + begin + pragma Assert (A /= B); + E := Get_First_Src_Edge (A); + while E /= No_Edge loop + Expr := Get_Edge_Expr (E); + Dest := Get_Edge_Dest (E); + if Expr /= Null_Node then + Add_Edge (B, Dest, Expr); + end if; + E := Get_Next_Src_Edge (E); + end loop; + end Duplicate_Src_Edges; + + -- All edges to A are duplicated using B as a destination. + -- Handle epsilon-edges. + procedure Duplicate_Dest_Edges (N : NFA; A, B : NFA_State) + is + pragma Unreferenced (N); + E : NFA_Edge; + Expr : Node; + Src : NFA_State; + begin + pragma Assert (A /= B); + E := Get_First_Dest_Edge (A); + while E /= No_Edge loop + Expr := Get_Edge_Expr (E); + Src := Get_Edge_Src (E); + if Expr /= Null_Node then + Add_Edge (Src, B, Expr); + end if; + E := Get_Next_Dest_Edge (E); + end loop; + end Duplicate_Dest_Edges; + + procedure Remove_Epsilon_Edge (N : NFA; S, D : NFA_State) is + begin + if Get_First_Src_Edge (S) = No_Edge then + -- No edge from S. + -- Move edges to S to D. + Redest_Edges (S, D); + Remove_Unconnected_State (N, S); + if Get_Start_State (N) = S then + Set_Start_State (N, D); + end if; + elsif Get_First_Dest_Edge (D) = No_Edge then + -- No edge to D. + -- Move edges from D to S. + Resource_Edges (D, S); + Remove_Unconnected_State (N, D); + if Get_Final_State (N) = D then + Set_Final_State (N, S); + end if; + else + Duplicate_Dest_Edges (N, S, D); + Duplicate_Src_Edges (N, D, S); + Remove_Identical_Src_Edges (S); + end if; + end Remove_Epsilon_Edge; + + procedure Remove_Epsilon (N : NFA; + E : NFA_Edge) is + S : constant NFA_State := Get_Edge_Src (E); + D : constant NFA_State := Get_Edge_Dest (E); + begin + Remove_Edge (E); + + Remove_Epsilon_Edge (N, S, D); + end Remove_Epsilon; + + function Build_Concat (L, R : NFA) return NFA + is + Start_L, Start_R : NFA_State; + Final_L, Final_R : NFA_State; + Eps_L, Eps_R : Boolean; + E_L, E_R : NFA_Edge; + begin + Start_L := Get_Start_State (L); + Start_R := Get_Start_State (R); + Final_R := Get_Final_State (R); + Final_L := Get_Final_State (L); + Eps_L := Get_Epsilon_NFA (L); + Eps_R := Get_Epsilon_NFA (R); + + Merge_NFA (L, R); + + Set_Start_State (L, Start_L); + Set_Final_State (L, Final_R); + Set_Epsilon_NFA (L, False); + + if Eps_L then + E_L := Add_Edge (Start_L, Final_L, Null_Node); + end if; + + if Eps_R then + E_R := Add_Edge (Start_R, Final_R, Null_Node); + end if; + + Remove_Epsilon_Edge (L, Final_L, Start_R); + + if Eps_L then + Remove_Epsilon (L, E_L); + end if; + if Eps_R then + Remove_Epsilon (L, E_R); + end if; + + if (Start_L = Final_L or else Eps_L) + and then (Start_R = Final_R or else Eps_R) + then + Set_Epsilon_NFA (L, True); + end if; + + Remove_Identical_Src_Edges (Final_L); + Remove_Identical_Dest_Edges (Start_R); + + return L; + end Build_Concat; + + function Build_Or (L, R : NFA) return NFA + is + Start_L, Start_R : NFA_State; + Final_L, Final_R : NFA_State; + Eps : Boolean; + Start, Final : NFA_State; + E_S_L, E_S_R, E_L_F, E_R_F : NFA_Edge; + begin + Start_L := Get_Start_State (L); + Start_R := Get_Start_State (R); + Final_R := Get_Final_State (R); + Final_L := Get_Final_State (L); + Eps := Get_Epsilon_NFA (L) or Get_Epsilon_NFA (R); + + -- Optimize [*0] | R. + if Start_L = Final_L + and then Get_First_Src_Edge (Start_L) = No_Edge + then + if Start_R /= Final_R then + Set_Epsilon_NFA (R, True); + end if; + -- FIXME + -- delete_NFA (L); + return R; + end if; + + Merge_NFA (L, R); + + -- Use Thompson construction. + Start := Add_State (L); + Set_Start_State (L, Start); + E_S_L := Add_Edge (Start, Start_L, Null_Node); + E_S_R := Add_Edge (Start, Start_R, Null_Node); + + Final := Add_State (L); + Set_Final_State (L, Final); + E_L_F := Add_Edge (Final_L, Final, Null_Node); + E_R_F := Add_Edge (Final_R, Final, Null_Node); + + Set_Epsilon_NFA (L, Eps); + + Remove_Epsilon (L, E_S_L); + Remove_Epsilon (L, E_S_R); + Remove_Epsilon (L, E_L_F); + Remove_Epsilon (L, E_R_F); + + return L; + end Build_Or; + + function Build_Fusion (L, R : NFA) return NFA + is + Start_R : NFA_State; + Final_L, Final_R, S_L : NFA_State; + E_L : NFA_Edge; + E_R : NFA_Edge; + N_L, Expr : Node; + begin + Start_R := Get_Start_State (R); + Final_R := Get_Final_State (R); + Final_L := Get_Final_State (L); + + Merge_NFA (L, R); + + E_L := Get_First_Dest_Edge (Final_L); + while E_L /= No_Edge loop + S_L := Get_Edge_Src (E_L); + N_L := Get_Edge_Expr (E_L); + + E_R := Get_First_Src_Edge (Start_R); + while E_R /= No_Edge loop + Expr := Build_Bool_And (N_L, Get_Edge_Expr (E_R)); + Expr := PSL.QM.Reduce (Expr); + if Expr /= False_Node then + Add_Edge (S_L, Get_Edge_Dest (E_R), Expr); + end if; + E_R := Get_Next_Src_Edge (E_R); + end loop; + Remove_Identical_Src_Edges (S_L); + E_L := Get_Next_Dest_Edge (E_L); + end loop; + + Set_Final_State (L, Final_R); + + Set_Epsilon_NFA (L, False); + + if Get_First_Src_Edge (Final_L) = No_Edge then + Remove_State (L, Final_L); + end if; + if Get_First_Dest_Edge (Start_R) = No_Edge then + Remove_State (L, Start_R); + end if; + + return L; + end Build_Fusion; + + function Build_Star_Repeat (N : Node) return NFA is + Res : NFA; + Start, Final, S : NFA_State; + Seq : Node; + begin + Seq := Get_Sequence (N); + if Seq = Null_Node then + -- Epsilon. + Res := Create_NFA; + S := Add_State (Res); + Set_Start_State (Res, S); + Set_Final_State (Res, S); + return Res; + end if; + Res := Build_SERE_FA (Seq); + Start := Get_Start_State (Res); + Final := Get_Final_State (Res); + Redest_Edges (Final, Start); + Set_Final_State (Res, Start); + Remove_Unconnected_State (Res, Final); + Set_Epsilon_NFA (Res, False); + return Res; + end Build_Star_Repeat; + + function Build_Plus_Repeat (N : Node) return NFA is + Res : NFA; + Start, Final : NFA_State; + T : NFA_Edge; + begin + Res := Build_SERE_FA (Get_Sequence (N)); + Start := Get_Start_State (Res); + Final := Get_Final_State (Res); + T := Get_First_Dest_Edge (Final); + while T /= No_Edge loop + Add_Edge (Get_Edge_Src (T), Start, Get_Edge_Expr (T)); + T := Get_Next_Src_Edge (T); + end loop; + return Res; + end Build_Plus_Repeat; + + -- Association actual to formals, so that when a formal is referenced, the + -- actual can be used instead. + procedure Assoc_Instance (Decl : Node; Instance : Node) + is + Formal : Node; + Actual : Node; + begin + -- Temporary associates actuals to formals. + Formal := Get_Parameter_List (Decl); + Actual := Get_Association_Chain (Instance); + while Formal /= Null_Node loop + if Actual = Null_Node then + -- Not enough actual. + raise Internal_Error; + end if; + if Get_Actual (Formal) /= Null_Node then + -- Recursion + raise Internal_Error; + end if; + Set_Actual (Formal, Get_Actual (Actual)); + Formal := Get_Chain (Formal); + Actual := Get_Chain (Actual); + end loop; + if Actual /= Null_Node then + -- Too many actual. + raise Internal_Error; + end if; + end Assoc_Instance; + + procedure Unassoc_Instance (Decl : Node) + is + Formal : Node; + begin + -- Remove temporary association. + Formal := Get_Parameter_List (Decl); + while Formal /= Null_Node loop + Set_Actual (Formal, Null_Node); + Formal := Get_Chain (Formal); + end loop; + end Unassoc_Instance; + + function Build_SERE_FA (N : Node) return NFA + is + Res : NFA; + S1, S2 : NFA_State; + begin + case Get_Kind (N) is + when N_Booleans => + Res := Create_NFA; + S1 := Add_State (Res); + S2 := Add_State (Res); + Set_Start_State (Res, S1); + Set_Final_State (Res, S2); + if N /= False_Node then + Add_Edge (S1, S2, N); + end if; + return Res; + when N_Braced_SERE => + return Build_SERE_FA (Get_SERE (N)); + when N_Concat_SERE => + return Build_Concat (Build_SERE_FA (Get_Left (N)), + Build_SERE_FA (Get_Right (N))); + when N_Fusion_SERE => + return Build_Fusion (Build_SERE_FA (Get_Left (N)), + Build_SERE_FA (Get_Right (N))); + when N_Match_And_Seq => + return Intersection.Build_Inter (Build_SERE_FA (Get_Left (N)), + Build_SERE_FA (Get_Right (N)), + True); + when N_And_Seq => + return Intersection.Build_Inter (Build_SERE_FA (Get_Left (N)), + Build_SERE_FA (Get_Right (N)), + False); + when N_Or_Prop + | N_Or_Seq => + return Build_Or (Build_SERE_FA (Get_Left (N)), + Build_SERE_FA (Get_Right (N))); + when N_Star_Repeat_Seq => + return Build_Star_Repeat (N); + when N_Plus_Repeat_Seq => + return Build_Plus_Repeat (N); + when N_Sequence_Instance + | N_Endpoint_Instance => + declare + Decl : Node; + begin + Decl := Get_Declaration (N); + Assoc_Instance (Decl, N); + Res := Build_SERE_FA (Get_Sequence (Decl)); + Unassoc_Instance (Decl); + return Res; + end; + when N_Boolean_Parameter + | N_Sequence_Parameter => + declare + Actual : constant Node := Get_Actual (N); + begin + if Actual = Null_Node then + raise Internal_Error; + end if; + return Build_SERE_FA (Actual); + end; + when others => + Error_Kind ("build_sere_fa", N); + end case; + end Build_SERE_FA; + + function Count_Edges (S : NFA_State) return Natural + is + Res : Natural; + E : NFA_Edge; + begin + Res := 0; + E := Get_First_Src_Edge (S); + while E /= No_Edge loop + Res := Res + 1; + E := Get_Next_Src_Edge (E); + end loop; + return Res; + end Count_Edges; + + type Count_Vector is array (Natural range <>) of Natural; + + procedure Count_All_Edges (N : NFA; Res : out Count_Vector) + is + S : NFA_State; + begin + S := Get_First_State (N); + while S /= No_State loop + Res (Natural (Get_State_Label (S))) := Count_Edges (S); + S := Get_Next_State (S); + end loop; + end Count_All_Edges; + + pragma Unreferenced (Count_All_Edges); + + package Determinize is + -- Create a new NFA that reaches its final state only when N fails + -- (ie when the final state is not reached). + function Determinize (N : NFA) return NFA; + end Determinize; + + package body Determinize is + -- In all the comments N stands for the initial NFA (ie the NFA to + -- determinize). + + use Prints; + + Flag_Trace : constant Boolean := False; + Last_Label : Int32 := 0; + + -- The tree associates a set of states in N to *an* uniq set in the + -- result NFA. + -- + -- As the NFA is labelized, each node represent a state in N, and has + -- two branches: one for state is present and one for state is absent. + -- + -- The leaves contain the state in the result NFA. + -- + -- The leaves are chained to create a stack of state to handle. + -- + -- The root of the tree is node Start_Tree_Id and represent the start + -- state of N. + type Deter_Tree_Id is new Natural; + No_Tree_Id : constant Deter_Tree_Id := 0; + Start_Tree_Id : constant Deter_Tree_Id := 1; + + -- List of unhanded leaves. + Deter_Head : Deter_Tree_Id; + + type Deter_Tree_Id_Bool_Array is array (Boolean) of Deter_Tree_Id; + + -- Node in the tree. + type Deter_Tree_Entry is record + Parent : Deter_Tree_Id; + + -- For non-leaf: + Child : Deter_Tree_Id_Bool_Array; + + -- For leaf: + Link : Deter_Tree_Id; + State : NFA_State; + -- + value ? + end record; + + package Detert is new GNAT.Table + (Table_Component_Type => Deter_Tree_Entry, + Table_Index_Type => Deter_Tree_Id, + Table_Low_Bound => 1, + Table_Initial => 128, + Table_Increment => 100); + + type Bool_Vector is array (Natural range <>) of Boolean; + pragma Pack (Bool_Vector); + + -- Convert a set of states in N to a state in the result NFA. + -- The set is represented by a vector of boolean. An element of the + -- vector is true iff the corresponding state is present. + function Add_Vector (V : Bool_Vector; N : NFA) return NFA_State + is + E : Deter_Tree_Id; + Added : Boolean; + Res : NFA_State; + begin + E := Start_Tree_Id; + Added := False; + for I in V'Range loop + if Detert.Table (E).Child (V (I)) = No_Tree_Id then + Detert.Append ((Child => (No_Tree_Id, No_Tree_Id), + Parent => E, + Link => No_Tree_Id, + State => No_State)); + Detert.Table (E).Child (V (I)) := Detert.Last; + E := Detert.Last; + Added := True; + else + E := Detert.Table (E).Child (V (I)); + Added := False; + end if; + end loop; + if Added then + -- Create the new state. + Res := Add_State (N); + Detert.Table (E).State := Res; + + if Flag_Trace then + Set_State_Label (Res, Last_Label); + Put ("Result state" & Int32'Image (Last_Label) & " for"); + for I in V'Range loop + if V (I) then + Put (Natural'Image (I)); + end if; + end loop; + New_Line; + Last_Label := Last_Label + 1; + end if; + + -- Put it to the list of states to be handled. + Detert.Table (E).Link := Deter_Head; + Deter_Head := E; + + return Res; + else + return Detert.Table (E).State; + end if; + end Add_Vector; + + -- Return true iff the stack is empty (ie all the states have been + -- handled). + function Stack_Empty return Boolean is + begin + return Deter_Head = No_Tree_Id; + end Stack_Empty; + + -- Get an element from the stack. + -- Extract the state in the result NFA. + -- Rebuild the set of states in N (ie rebuild the vector of states). + procedure Stack_Pop (V : out Bool_Vector; S : out NFA_State) + is + L, P : Deter_Tree_Id; + begin + L := Deter_Head; + pragma Assert (L /= No_Tree_Id); + S := Detert.Table (L).State; + Deter_Head := Detert.Table (L).Link; + + for I in reverse V'Range loop + pragma Assert (L /= Start_Tree_Id); + P := Detert.Table (L).Parent; + if L = Detert.Table (P).Child (True) then + V (I) := True; + elsif L = Detert.Table (P).Child (False) then + V (I) := False; + else + raise Program_Error; + end if; + L := P; + end loop; + pragma Assert (L = Start_Tree_Id); + end Stack_Pop; + + type State_Vector is array (Natural range <>) of Natural; + type Expr_Vector is array (Natural range <>) of Node; + + procedure Build_Arcs (N : NFA; + State : NFA_State; + States : State_Vector; + Exprs : Expr_Vector; + Expr : Node; + V : Bool_Vector) + is + begin + if Expr = False_Node then + return; + end if; + + if States'Length = 0 then + declare + Reduced_Expr : constant Node := PSL.QM.Reduce (Expr); + --Reduced_Expr : constant Node := Expr; + S : NFA_State; + begin + if Reduced_Expr = False_Node then + return; + end if; + S := Add_Vector (V, N); + Add_Edge (State, S, Reduced_Expr); + if Flag_Trace then + Put (" Add edge"); + Put (Int32'Image (Get_State_Label (State))); + Put (" to"); + Put (Int32'Image (Get_State_Label (S))); + Put (", expr="); + Dump_Expr (Expr); + Put (", reduced="); + Dump_Expr (Reduced_Expr); + New_Line; + end if; + end; + else + declare + N_States : State_Vector renames + States (States'First + 1 .. States'Last); + N_V : Bool_Vector (V'Range) := V; + S : constant Natural := States (States'First); + E : constant Node := Exprs (S); + begin + N_V (S) := True; + if Expr = Null_Node then + Build_Arcs (N, State, N_States, Exprs, E, N_V); + Build_Arcs (N, State, N_States, Exprs, + Build_Bool_Not (E), V); + else + Build_Arcs (N, State, N_States, Exprs, + Build_Bool_And (E, Expr), N_V); + Build_Arcs (N, State, N_States, Exprs, + Build_Bool_And (Build_Bool_Not (E), Expr), V); + end if; + end; + end if; + end Build_Arcs; + + function Determinize_1 (N : NFA; Nbr_States : Natural) return NFA + is + Final : Natural; + V : Bool_Vector (0 .. Nbr_States - 1); + Exprs : Expr_Vector (0 .. Nbr_States - 1); + S : NFA_State; + E : NFA_Edge; + D : Natural; + Edge_Expr : Node; + Expr : Node; + Nbr_Dest : Natural; + States : State_Vector (0 .. Nbr_States - 1); + Res : NFA; + State : NFA_State; + begin + Final := Natural (Get_State_Label (Get_Final_State (N))); + + -- FIXME: handle epsilon or final = start -> create an empty NFA. + + -- Initialize the tree. + Res := Create_NFA; + Detert.Init; + Detert.Append ((Child => (No_Tree_Id, No_Tree_Id), + Parent => No_Tree_Id, + Link => No_Tree_Id, + State => No_State)); + pragma Assert (Detert.Last = Start_Tree_Id); + Deter_Head := No_Tree_Id; + + -- Put the initial state in the tree and in the stack. + -- FIXME: ok, we know that its label is 0. + V := (0 => True, others => False); + State := Add_Vector (V, Res); + Set_Start_State (Res, State); + + -- The failure state. As there is nothing to do with this + -- state, remove it from the stack. + V := (others => False); + State := Add_Vector (V, Res); + Set_Final_State (Res, State); + Stack_Pop (V, State); + + -- Iterate on states in the result NFA that haven't yet been handled. + while not Stack_Empty loop + Stack_Pop (V, State); + + if Flag_Trace then + Put_Line ("Handle result state" + & Int32'Image (Get_State_Label (State))); + end if; + + -- Build edges vector. + Exprs := (others => Null_Node); + Expr := Null_Node; + + S := Get_First_State (N); + Nbr_Dest := 0; + while S /= No_State loop + if V (Natural (Get_State_Label (S))) then + E := Get_First_Src_Edge (S); + while E /= No_Edge loop + D := Natural (Get_State_Label (Get_Edge_Dest (E))); + Edge_Expr := Get_Edge_Expr (E); + + if False and Flag_Trace then + Put_Line (" edge" & Int32'Image (Get_State_Label (S)) + & " to" & Natural'Image (D)); + end if; + + if D = Final then + Edge_Expr := Build_Bool_Not (Edge_Expr); + if Expr = Null_Node then + Expr := Edge_Expr; + else + Expr := Build_Bool_And (Expr, Edge_Expr); + end if; + else + if Exprs (D) = Null_Node then + Exprs (D) := Edge_Expr; + States (Nbr_Dest) := D; + Nbr_Dest := Nbr_Dest + 1; + else + Exprs (D) := Build_Bool_Or (Exprs (D), + Edge_Expr); + end if; + end if; + E := Get_Next_Src_Edge (E); + end loop; + end if; + S := Get_Next_State (S); + end loop; + + if Flag_Trace then + Put (" Final: expr="); + Print_Expr (Expr); + New_Line; + for I in 0 .. Nbr_Dest - 1 loop + Put (" Dest"); + Put (Natural'Image (States (I))); + Put (" expr="); + Print_Expr (Exprs (States (I))); + New_Line; + end loop; + end if; + + -- Build arcs. + if not (Nbr_Dest = 0 and Expr = Null_Node) then + Build_Arcs (Res, State, + States (0 .. Nbr_Dest - 1), Exprs, Expr, + Bool_Vector'(0 .. Nbr_States - 1 => False)); + end if; + end loop; + + --Remove_Unreachable_States (Res); + return Res; + end Determinize_1; + + function Determinize (N : NFA) return NFA + is + Nbr_States : Natural; + begin + Labelize_States (N, Nbr_States); + + if Flag_Trace then + Put_Line ("NFA to determinize:"); + Disp_NFA (N); + Last_Label := 0; + end if; + + return Determinize_1 (N, Nbr_States); + end Determinize; + end Determinize; + + function Build_Initial_Rep (N : NFA) return NFA + is + S : constant NFA_State := Get_Start_State (N); + begin + Add_Edge (S, S, True_Node); + return N; + end Build_Initial_Rep; + + procedure Build_Strong (N : NFA) + is + S : NFA_State; + Final : constant NFA_State := Get_Final_State (N); + begin + S := Get_First_State (N); + while S /= No_State loop + -- FIXME. + if S /= Final then + Add_Edge (S, Final, EOS_Node); + end if; + S := Get_Next_State (S); + end loop; + end Build_Strong; + + procedure Build_Abort (N : NFA; Expr : Node) + is + S : NFA_State; + E : NFA_Edge; + Not_Expr : Node; + begin + Not_Expr := Build_Bool_Not (Expr); + S := Get_First_State (N); + while S /= No_State loop + E := Get_First_Src_Edge (S); + while E /= No_Edge loop + Set_Edge_Expr (E, Build_Bool_And (Not_Expr, Get_Edge_Expr (E))); + E := Get_Next_Src_Edge (E); + end loop; + S := Get_Next_State (S); + end loop; + end Build_Abort; + + function Build_Property_FA (N : Node) return NFA + is + L, R : NFA; + begin + case Get_Kind (N) is + when N_Sequences + | N_Booleans => + -- Build A(S) or A(B) + R := Build_SERE_FA (N); + return Determinize.Determinize (R); + when N_Strong => + R := Build_Property_FA (Get_Property (N)); + Build_Strong (R); + return R; + when N_Imp_Seq => + -- R |=> P --> {R; TRUE} |-> P + L := Build_SERE_FA (Get_Sequence (N)); + R := Build_Property_FA (Get_Property (N)); + return Build_Concat (L, R); + when N_Overlap_Imp_Seq => + -- S |-> P is defined as Ac(S) : A(P) + L := Build_SERE_FA (Get_Sequence (N)); + R := Build_Property_FA (Get_Property (N)); + return Build_Fusion (L, R); + when N_Log_Imp_Prop => + -- B -> P --> {B} |-> P --> Ac(B) : A(P) + L := Build_SERE_FA (Get_Left (N)); + R := Build_Property_FA (Get_Right (N)); + return Build_Fusion (L, R); + when N_And_Prop => + -- P1 && P2 --> A(P1) | A(P2) + L := Build_Property_FA (Get_Left (N)); + R := Build_Property_FA (Get_Right (N)); + return Build_Or (L, R); + when N_Never => + R := Build_SERE_FA (Get_Property (N)); + return Build_Initial_Rep (R); + when N_Always => + R := Build_Property_FA (Get_Property (N)); + return Build_Initial_Rep (R); + when N_Abort => + R := Build_Property_FA (Get_Property (N)); + Build_Abort (R, Get_Boolean (N)); + return R; + when N_Property_Instance => + declare + Decl : Node; + begin + Decl := Get_Declaration (N); + Assoc_Instance (Decl, N); + R := Build_Property_FA (Get_Property (Decl)); + Unassoc_Instance (Decl); + return R; + end; + when others => + Error_Kind ("build_property_fa", N); + end case; + end Build_Property_FA; + + function Build_FA (N : Node) return NFA + is + use PSL.NFAs.Utils; + Res : NFA; + begin + Res := Build_Property_FA (N); + if Optimize_Final then + pragma Debug (Check_NFA (Res)); + + Remove_Unreachable_States (Res); + Remove_Simple_Prefix (Res); + Merge_Identical_States (Res); + Merge_Edges (Res); + end if; + -- Clear the QM table. + PSL.QM.Reset; + return Res; + end Build_FA; +end PSL.Build; diff --git a/src/psl/psl-build.ads b/src/psl/psl-build.ads new file mode 100644 index 000000000..d0ca26a39 --- /dev/null +++ b/src/psl/psl-build.ads @@ -0,0 +1,7 @@ +with PSL.Nodes; use PSL.Nodes; + +package PSL.Build is + Optimize_Final : Boolean := True; + + function Build_FA (N : Node) return NFA; +end PSL.Build; diff --git a/src/psl/psl-cse.adb b/src/psl/psl-cse.adb new file mode 100644 index 000000000..5d6f3df13 --- /dev/null +++ b/src/psl/psl-cse.adb @@ -0,0 +1,201 @@ +with Ada.Text_IO; +with PSL.Prints; +with Types; use Types; + +package body PSL.CSE is + function Is_X_And_Not_X (A, B : Node) return Boolean is + begin + return (Get_Kind (A) = N_Not_Bool + and then Get_Boolean (A) = B) + or else (Get_Kind (B) = N_Not_Bool + and then Get_Boolean (B) = A); + end Is_X_And_Not_X; + + type Hash_Table_Type is array (Uns32 range 0 .. 128) of Node; + Hash_Table : Hash_Table_Type := (others => Null_Node); + + function Compute_Hash (L, R : Node; Op : Uns32) return Uns32 + is + begin + return Shift_Left (Get_Hash (L), 12) + xor Shift_Left (Get_Hash (R), 2) + xor Op; + end Compute_Hash; + + function Compute_Hash (L: Node; Op : Uns32) return Uns32 + is + begin + return Shift_Left (Get_Hash (L), 2) xor Op; + end Compute_Hash; + + procedure Dump_Hash_Table (Level : Natural := 0) + is + use Ada.Text_IO; + Cnt : Natural; + Total : Natural; + N : Node; + begin + Total := 0; + for I in Hash_Table_Type'Range loop + Cnt := 0; + N := Hash_Table (I); + while N /= Null_Node loop + Cnt := Cnt + 1; + N := Get_Hash_Link (N); + end loop; + Put_Line ("Hash_table(" & Uns32'Image (I) + & "):" & Natural'Image (Cnt)); + Total := Total + Cnt; + if Level > 0 then + Cnt := 0; + N := Hash_Table (I); + while N /= Null_Node loop + Put (Uns32'Image (Get_Hash (N))); + if Level > 1 then + Put (": "); + PSL.Prints.Dump_Expr (N); + New_Line; + end if; + Cnt := Cnt + 1; + N := Get_Hash_Link (N); + end loop; + if Level = 1 and then Cnt > 0 then + New_Line; + end if; + end if; + end loop; + Put_Line ("Total:" & Natural'Image (Total)); + end Dump_Hash_Table; + + function Build_Bool_And (L, R : Node) return Node + is + R1 : Node; + Res : Node; + Hash : Uns32; + Head, H : Node; + begin + if L = True_Node then + return R; + elsif R = True_Node then + return L; + elsif L = False_Node or else R = False_Node then + return False_Node; + elsif L = R then + return L; + elsif Is_X_And_Not_X (L, R) then + return False_Node; + end if; + + -- More simple optimizations. + if Get_Kind (R) = N_And_Bool then + R1 := Get_Left (R); + if L = R1 then + return R; + elsif Is_X_And_Not_X (L, R1) then + return False_Node; + end if; + end if; + + Hash := Compute_Hash (L, R, 2); + Head := Hash_Table (Hash mod Hash_Table'Length); + H := Head; + while H /= Null_Node loop + if Get_Hash (H) = Hash + and then Get_Kind (H) = N_And_Bool + and then Get_Left (H) = L + and then Get_Right (H) = R + then + return H; + end if; + H := Get_Hash_Link (H); + end loop; + + Res := Create_Node (N_And_Bool); + Set_Left (Res, L); + Set_Right (Res, R); + Set_Hash_Link (Res, Head); + Set_Hash (Res, Hash); + Hash_Table (Hash mod Hash_Table'Length) := Res; + return Res; + end Build_Bool_And; + + function Build_Bool_Or (L, R : Node) return Node + is + Res : Node; + Hash : Uns32; + Head, H : Node; + begin + if L = True_Node then + return L; + elsif R = True_Node then + return R; + elsif L = False_Node then + return R; + elsif R = False_Node then + return L; + elsif L = R then + return L; + elsif Is_X_And_Not_X (L, R) then + return True_Node; + end if; + + Hash := Compute_Hash (L, R, 3); + Head := Hash_Table (Hash mod Hash_Table'Length); + H := Head; + while H /= Null_Node loop + if Get_Hash (H) = Hash + and then Get_Kind (H) = N_Or_Bool + and then Get_Left (H) = L + and then Get_Right (H) = R + then + return H; + end if; + H := Get_Hash_Link (H); + end loop; + + Res := Create_Node (N_Or_Bool); + Set_Left (Res, L); + Set_Right (Res, R); + Set_Hash_Link (Res, Head); + Set_Hash (Res, Hash); + Hash_Table (Hash mod Hash_Table'Length) := Res; + return Res; + end Build_Bool_Or; + + function Build_Bool_Not (N : Node) return Node is + Res : Node; + Hash : Uns32; + Head : Node; + H : Node; + begin + if N = True_Node then + return False_Node; + elsif N = False_Node then + return True_Node; + elsif Get_Kind (N) = N_Not_Bool then + return Get_Boolean (N); + end if; + + -- Find in hash table. + Hash := Compute_Hash (N, 1); + Head := Hash_Table (Hash mod Hash_Table'Length); + H := Head; + while H /= Null_Node loop + if Get_Hash (H) = Hash + and then Get_Kind (H) = N_Not_Bool + and then Get_Boolean (H) = N + then + return H; + end if; + H := Get_Hash_Link (H); + end loop; + + Res := Create_Node (N_Not_Bool); + Set_Boolean (Res, N); + Set_Hash_Link (Res, Head); + Set_Hash (Res, Hash); + Hash_Table (Hash mod Hash_Table'Length) := Res; + + return Res; + end Build_Bool_Not; +end PSL.CSE; diff --git a/src/psl/psl-cse.ads b/src/psl/psl-cse.ads new file mode 100644 index 000000000..e40b0eeb2 --- /dev/null +++ b/src/psl/psl-cse.ads @@ -0,0 +1,10 @@ +with PSL.Nodes; use PSL.Nodes; + +package PSL.CSE is + -- Build boolean expressions while trying to make the node uniq. + function Build_Bool_And (L, R : Node) return Node; + function Build_Bool_Or (L, R : Node) return Node; + function Build_Bool_Not (N : Node) return Node; + + procedure Dump_Hash_Table (Level : Natural := 0); +end PSL.CSE; diff --git a/src/psl/psl-disp_nfas.adb b/src/psl/psl-disp_nfas.adb new file mode 100644 index 000000000..c8f1532b9 --- /dev/null +++ b/src/psl/psl-disp_nfas.adb @@ -0,0 +1,111 @@ +with Ada.Text_IO; use Ada.Text_IO; +with Types; use Types; +with PSL.Prints; use PSL.Prints; + +package body PSL.Disp_NFAs is + procedure Disp_State (S : NFA_State) is + Str : constant String := Int32'Image (Get_State_Label (S)); + begin + Put (Str (2 .. Str'Last)); + end Disp_State; + + procedure Disp_Head (Name : String) is + begin + Put ("digraph "); + Put (Name); + Put_Line (" {"); + Put_Line (" rankdir=LR;"); + end Disp_Head; + + procedure Disp_Tail is + begin + Put_Line ("}"); + end Disp_Tail; + + procedure Disp_Body (N : NFA) is + S, F : NFA_State; + T : NFA_Edge; + begin + S := Get_Start_State (N); + F := Get_Final_State (N); + if S /= No_State then + if S = F then + Put (" node [shape = doublecircle, style = bold];"); + else + Put (" node [shape = circle, style = bold];"); + end if; + Put (" /* Start: */ "); + Disp_State (S); + Put_Line (";"); + end if; + if F /= No_State and then F /= S then + Put (" node [shape = doublecircle, style = solid];"); + Put (" /* Final: */ "); + Disp_State (F); + Put_Line (";"); + end if; + Put_Line (" node [shape = circle, style = solid];"); + + if Get_Epsilon_NFA (N) then + Put (" "); + Disp_State (Get_Start_State (N)); + Put (" -> "); + Disp_State (Get_Final_State (N)); + Put_Line (" [ label = ""*""]"); + end if; + + S := Get_First_State (N); + while S /= No_State loop + T := Get_First_Src_Edge (S); + if T = No_Edge then + if Get_First_Dest_Edge (S) = No_Edge then + Put (" "); + Disp_State (S); + Put_Line (";"); + end if; + else + loop + Put (" "); + Disp_State (S); + Put (" -> "); + Disp_State (Get_Edge_Dest (T)); + Put (" [ label = """); + Print_Expr (Get_Edge_Expr (T)); + Put ('"'); + if True then + Put (" /* Node ="); + Put (Node'Image (Get_Edge_Expr (T))); + Put (" */"); + end if; + if True then + Put (" /* Edge ="); + Put (NFA_Edge'Image (T)); + Put (" */"); + end if; + Put_Line (" ];"); + + T := Get_Next_Src_Edge (T); + exit when T = No_Edge; + end loop; + end if; + S := Get_Next_State (S); + end loop; + end Disp_Body; + + procedure Disp_NFA (N : NFA; Name : String := "nfa") is + begin + Disp_Head (Name); + Disp_Body (N); + Disp_Tail; + end Disp_NFA; + + procedure Debug_NFA (N : NFA) is + begin + Labelize_States_Debug (N); + Disp_Head ("nfa"); + Disp_Body (N); + Disp_Tail; + end Debug_NFA; + + pragma Unreferenced (Debug_NFA); +end PSL.Disp_NFAs; diff --git a/src/psl/psl-disp_nfas.ads b/src/psl/psl-disp_nfas.ads new file mode 100644 index 000000000..901eed72f --- /dev/null +++ b/src/psl/psl-disp_nfas.ads @@ -0,0 +1,12 @@ +with PSL.NFAs; use PSL.NFAs; +with PSL.Nodes; use PSL.Nodes; + +package PSL.Disp_NFAs is + procedure Disp_Head (Name : String); + procedure Disp_Tail; + procedure Disp_Body (N : NFA); + + procedure Disp_State (S : NFA_State); + + procedure Disp_NFA (N : NFA; Name : String := "nfa"); +end PSL.Disp_NFAs; diff --git a/src/psl/psl-dump_tree.adb b/src/psl/psl-dump_tree.adb new file mode 100644 index 000000000..db636dbb0 --- /dev/null +++ b/src/psl/psl-dump_tree.adb @@ -0,0 +1,867 @@ +-- This is in fact -*- Ada -*- +with Ada.Text_IO; use Ada.Text_IO; +with Types; use Types; +with Name_Table; +with PSL.Errors; + +package body PSL.Dump_Tree is + + procedure Disp_Indent (Indent : Natural) is + begin + Put (String'(1 .. 2 * Indent => ' ')); + end Disp_Indent; + + Hex_Digits : constant array (Integer range 0 .. 15) of Character + := "0123456789abcdef"; + + procedure Disp_Uns32 (Val : Uns32) + is + Res : String (1 .. 8); + V : Uns32 := Val; + begin + for I in reverse Res'Range loop + Res (I) := Hex_Digits (Integer (V mod 16)); + V := V / 16; + end loop; + Put (Res); + end Disp_Uns32; + + procedure Disp_Int32 (Val : Int32) + is + Res : String (1 .. 8); + V : Int32 := Val; + begin + for I in reverse Res'Range loop + Res (I) := Hex_Digits (Integer (V mod 16)); + V := V / 16; + end loop; + Put (Res); + end Disp_Int32; + + procedure Disp_HDL_Node (Val : HDL_Node) + is + begin + if Dump_Hdl_Node /= null then + Dump_Hdl_Node.all (Val); + else + Disp_Int32 (Val); + end if; + end Disp_HDL_Node; + + procedure Disp_Node_Number (N : Node) is + begin + Put ('['); + Disp_Int32 (Int32 (N)); + Put (']'); + end Disp_Node_Number; + + procedure Disp_NFA (Val : NFA) is + begin + Disp_Int32 (Int32 (Val)); + end Disp_NFA; + + procedure Disp_Header (Msg : String; Indent : Natural) is + begin + Disp_Indent (Indent); + Put (Msg); + Put (": "); + end Disp_Header; + + procedure Disp_Identifier (N : Node) is + begin + Put (Name_Table.Image (Get_Identifier (N))); + New_Line; + end Disp_Identifier; + + procedure Disp_Label (N : Node) is + begin + Put (Name_Table.Image (Get_Label (N))); + New_Line; + end Disp_Label; + + procedure Disp_Boolean (Val : Boolean) is + begin + if Val then + Put ("true"); + else + Put ("false"); + end if; + end Disp_Boolean; + + procedure Disp_PSL_Presence_Kind (Pres : PSL_Presence_Kind) is + begin + case Pres is + when Present_Pos => + Put ('+'); + when Present_Neg => + Put ('-'); + when Present_Unknown => + Put ('?'); + end case; + end Disp_PSL_Presence_Kind; + + procedure Disp_Location (Loc : Location_Type) is + begin + Put (PSL.Errors.Get_Location_Str (Loc)); + end Disp_Location; + +-- procedure Disp_String_Id (N : Node) is +-- begin +-- Put ('"'); +-- Put (Str_Table.Image (Get_String_Id (N))); +-- Put ('"'); +-- New_Line; +-- end Disp_String_Id; + + -- Subprograms. + procedure Disp_Tree (N : Node; Indent : Natural; Full : boolean := False) is + begin + Disp_Indent (Indent); + Disp_Node_Number (N); + Put (": "); + if N = Null_Node then + Put_Line ("*NULL*"); + return; + end if; + Put_Line (Nkind'Image (Get_Kind (N))); + Disp_Indent (Indent); + Put ("loc: "); + Disp_Location (Get_Location (N)); + New_Line; + case Get_Kind (N) is + when N_Error => + if not Full then + return; + end if; + null; + when N_Vmode => + Disp_Header ("Identifier", Indent + 1); + Disp_Identifier (N); + if not Full then + return; + end if; + Disp_Header ("Instance", Indent + 1); + New_Line; + Disp_Tree (Get_Instance (N), Indent + 1, Full); + Disp_Header ("Item_Chain", Indent + 1); + New_Line; + Disp_Tree (Get_Item_Chain (N), Indent + 1, Full); + Disp_Tree (Get_Chain (N), Indent, Full); + null; + when N_Vunit => + Disp_Header ("Identifier", Indent + 1); + Disp_Identifier (N); + if not Full then + return; + end if; + Disp_Header ("Instance", Indent + 1); + New_Line; + Disp_Tree (Get_Instance (N), Indent + 1, Full); + Disp_Header ("Item_Chain", Indent + 1); + New_Line; + Disp_Tree (Get_Item_Chain (N), Indent + 1, Full); + Disp_Tree (Get_Chain (N), Indent, Full); + null; + when N_Vprop => + Disp_Header ("Identifier", Indent + 1); + Disp_Identifier (N); + if not Full then + return; + end if; + Disp_Header ("Instance", Indent + 1); + New_Line; + Disp_Tree (Get_Instance (N), Indent + 1, Full); + Disp_Header ("Item_Chain", Indent + 1); + New_Line; + Disp_Tree (Get_Item_Chain (N), Indent + 1, Full); + Disp_Tree (Get_Chain (N), Indent, Full); + null; + when N_Hdl_Mod_Name => + Disp_Header ("Identifier", Indent + 1); + Disp_Identifier (N); + if not Full then + return; + end if; + Disp_Header ("Prefix", Indent + 1); + New_Line; + Disp_Tree (Get_Prefix (N), Indent + 1, Full); + null; + when N_Assert_Directive => + Disp_Header ("Label", Indent + 1); + Disp_Label (N); + if not Full then + return; + end if; + Disp_Header ("String", Indent + 1); + New_Line; + Disp_Tree (Get_String (N), Indent + 1, Full); + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + Disp_Header ("NFA", Indent + 1); + Disp_NFA (Get_NFA (N)); + New_Line; + Disp_Tree (Get_Chain (N), Indent, Full); + null; + when N_Property_Declaration => + Disp_Header ("Identifier", Indent + 1); + Disp_Identifier (N); + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + Disp_Header ("Global_Clock", Indent + 1); + New_Line; + Disp_Tree (Get_Global_Clock (N), Indent + 1, Full); + Disp_Header ("Parameter_List", Indent + 1); + New_Line; + Disp_Tree (Get_Parameter_List (N), Indent + 1, Full); + Disp_Tree (Get_Chain (N), Indent, Full); + null; + when N_Sequence_Declaration => + Disp_Header ("Identifier", Indent + 1); + Disp_Identifier (N); + if not Full then + return; + end if; + Disp_Header ("Parameter_List", Indent + 1); + New_Line; + Disp_Tree (Get_Parameter_List (N), Indent + 1, Full); + Disp_Header ("Sequence", Indent + 1); + New_Line; + Disp_Tree (Get_Sequence (N), Indent + 1, Full); + Disp_Tree (Get_Chain (N), Indent, Full); + null; + when N_Endpoint_Declaration => + Disp_Header ("Identifier", Indent + 1); + Disp_Identifier (N); + if not Full then + return; + end if; + Disp_Header ("Parameter_List", Indent + 1); + New_Line; + Disp_Tree (Get_Parameter_List (N), Indent + 1, Full); + Disp_Header ("Sequence", Indent + 1); + New_Line; + Disp_Tree (Get_Sequence (N), Indent + 1, Full); + Disp_Tree (Get_Chain (N), Indent, Full); + null; + when N_Const_Parameter => + Disp_Header ("Identifier", Indent + 1); + Disp_Identifier (N); + if not Full then + return; + end if; + Disp_Header ("Actual", Indent + 1); + New_Line; + Disp_Tree (Get_Actual (N), Indent + 1, Full); + Disp_Tree (Get_Chain (N), Indent, Full); + null; + when N_Boolean_Parameter => + Disp_Header ("Identifier", Indent + 1); + Disp_Identifier (N); + if not Full then + return; + end if; + Disp_Header ("Actual", Indent + 1); + New_Line; + Disp_Tree (Get_Actual (N), Indent + 1, Full); + Disp_Tree (Get_Chain (N), Indent, Full); + null; + when N_Property_Parameter => + Disp_Header ("Identifier", Indent + 1); + Disp_Identifier (N); + if not Full then + return; + end if; + Disp_Header ("Actual", Indent + 1); + New_Line; + Disp_Tree (Get_Actual (N), Indent + 1, Full); + Disp_Tree (Get_Chain (N), Indent, Full); + null; + when N_Sequence_Parameter => + Disp_Header ("Identifier", Indent + 1); + Disp_Identifier (N); + if not Full then + return; + end if; + Disp_Header ("Actual", Indent + 1); + New_Line; + Disp_Tree (Get_Actual (N), Indent + 1, Full); + Disp_Tree (Get_Chain (N), Indent, Full); + null; + when N_Sequence_Instance => + if not Full then + return; + end if; + Disp_Header ("Declaration", Indent + 1); + New_Line; + Disp_Tree (Get_Declaration (N), Indent + 1, False); + Disp_Header ("Association_Chain", Indent + 1); + New_Line; + Disp_Tree (Get_Association_Chain (N), Indent + 1, Full); + null; + when N_Endpoint_Instance => + if not Full then + return; + end if; + Disp_Header ("Declaration", Indent + 1); + New_Line; + Disp_Tree (Get_Declaration (N), Indent + 1, False); + Disp_Header ("Association_Chain", Indent + 1); + New_Line; + Disp_Tree (Get_Association_Chain (N), Indent + 1, Full); + null; + when N_Property_Instance => + if not Full then + return; + end if; + Disp_Header ("Declaration", Indent + 1); + New_Line; + Disp_Tree (Get_Declaration (N), Indent + 1, False); + Disp_Header ("Association_Chain", Indent + 1); + New_Line; + Disp_Tree (Get_Association_Chain (N), Indent + 1, Full); + null; + when N_Actual => + if not Full then + return; + end if; + Disp_Header ("Actual", Indent + 1); + New_Line; + Disp_Tree (Get_Actual (N), Indent + 1, Full); + Disp_Header ("Formal", Indent + 1); + New_Line; + Disp_Tree (Get_Formal (N), Indent + 1, Full); + Disp_Tree (Get_Chain (N), Indent, Full); + null; + when N_Clock_Event => + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + Disp_Header ("Boolean", Indent + 1); + New_Line; + Disp_Tree (Get_Boolean (N), Indent + 1, Full); + null; + when N_Always => + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + null; + when N_Never => + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + null; + when N_Eventually => + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + null; + when N_Strong => + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + null; + when N_Imp_Seq => + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + Disp_Header ("Sequence", Indent + 1); + New_Line; + Disp_Tree (Get_Sequence (N), Indent + 1, Full); + null; + when N_Overlap_Imp_Seq => + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + Disp_Header ("Sequence", Indent + 1); + New_Line; + Disp_Tree (Get_Sequence (N), Indent + 1, Full); + null; + when N_Log_Imp_Prop => + if not Full then + return; + end if; + Disp_Header ("Left", Indent + 1); + New_Line; + Disp_Tree (Get_Left (N), Indent + 1, Full); + Disp_Header ("Right", Indent + 1); + New_Line; + Disp_Tree (Get_Right (N), Indent + 1, Full); + null; + when N_Next => + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + Disp_Header ("Strong_Flag", Indent + 1); + Disp_Boolean (Get_Strong_Flag (N)); + New_Line; + Disp_Header ("Number", Indent + 1); + New_Line; + Disp_Tree (Get_Number (N), Indent + 1, Full); + null; + when N_Next_A => + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + Disp_Header ("Strong_Flag", Indent + 1); + Disp_Boolean (Get_Strong_Flag (N)); + New_Line; + Disp_Header ("Low_Bound", Indent + 1); + New_Line; + Disp_Tree (Get_Low_Bound (N), Indent + 1, Full); + Disp_Header ("High_Bound", Indent + 1); + New_Line; + Disp_Tree (Get_High_Bound (N), Indent + 1, Full); + null; + when N_Next_E => + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + Disp_Header ("Strong_Flag", Indent + 1); + Disp_Boolean (Get_Strong_Flag (N)); + New_Line; + Disp_Header ("Low_Bound", Indent + 1); + New_Line; + Disp_Tree (Get_Low_Bound (N), Indent + 1, Full); + Disp_Header ("High_Bound", Indent + 1); + New_Line; + Disp_Tree (Get_High_Bound (N), Indent + 1, Full); + null; + when N_Next_Event => + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + Disp_Header ("Boolean", Indent + 1); + New_Line; + Disp_Tree (Get_Boolean (N), Indent + 1, Full); + Disp_Header ("Strong_Flag", Indent + 1); + Disp_Boolean (Get_Strong_Flag (N)); + New_Line; + Disp_Header ("Number", Indent + 1); + New_Line; + Disp_Tree (Get_Number (N), Indent + 1, Full); + null; + when N_Next_Event_A => + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + Disp_Header ("Boolean", Indent + 1); + New_Line; + Disp_Tree (Get_Boolean (N), Indent + 1, Full); + Disp_Header ("Strong_Flag", Indent + 1); + Disp_Boolean (Get_Strong_Flag (N)); + New_Line; + Disp_Header ("Low_Bound", Indent + 1); + New_Line; + Disp_Tree (Get_Low_Bound (N), Indent + 1, Full); + Disp_Header ("High_Bound", Indent + 1); + New_Line; + Disp_Tree (Get_High_Bound (N), Indent + 1, Full); + null; + when N_Next_Event_E => + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + Disp_Header ("Boolean", Indent + 1); + New_Line; + Disp_Tree (Get_Boolean (N), Indent + 1, Full); + Disp_Header ("Strong_Flag", Indent + 1); + Disp_Boolean (Get_Strong_Flag (N)); + New_Line; + Disp_Header ("Low_Bound", Indent + 1); + New_Line; + Disp_Tree (Get_Low_Bound (N), Indent + 1, Full); + Disp_Header ("High_Bound", Indent + 1); + New_Line; + Disp_Tree (Get_High_Bound (N), Indent + 1, Full); + null; + when N_Abort => + if not Full then + return; + end if; + Disp_Header ("Property", Indent + 1); + New_Line; + Disp_Tree (Get_Property (N), Indent + 1, Full); + Disp_Header ("Boolean", Indent + 1); + New_Line; + Disp_Tree (Get_Boolean (N), Indent + 1, Full); + null; + when N_Until => + if not Full then + return; + end if; + Disp_Header ("Strong_Flag", Indent + 1); + Disp_Boolean (Get_Strong_Flag (N)); + New_Line; + Disp_Header ("Left", Indent + 1); + New_Line; + Disp_Tree (Get_Left (N), Indent + 1, Full); + Disp_Header ("Right", Indent + 1); + New_Line; + Disp_Tree (Get_Right (N), Indent + 1, Full); + Disp_Header ("Inclusive_Flag", Indent + 1); + Disp_Boolean (Get_Inclusive_Flag (N)); + New_Line; + null; + when N_Before => + if not Full then + return; + end if; + Disp_Header ("Strong_Flag", Indent + 1); + Disp_Boolean (Get_Strong_Flag (N)); + New_Line; + Disp_Header ("Left", Indent + 1); + New_Line; + Disp_Tree (Get_Left (N), Indent + 1, Full); + Disp_Header ("Right", Indent + 1); + New_Line; + Disp_Tree (Get_Right (N), Indent + 1, Full); + Disp_Header ("Inclusive_Flag", Indent + 1); + Disp_Boolean (Get_Inclusive_Flag (N)); + New_Line; + null; + when N_Or_Prop => + if not Full then + return; + end if; + Disp_Header ("Left", Indent + 1); + New_Line; + Disp_Tree (Get_Left (N), Indent + 1, Full); + Disp_Header ("Right", Indent + 1); + New_Line; + Disp_Tree (Get_Right (N), Indent + 1, Full); + null; + when N_And_Prop => + if not Full then + return; + end if; + Disp_Header ("Left", Indent + 1); + New_Line; + Disp_Tree (Get_Left (N), Indent + 1, Full); + Disp_Header ("Right", Indent + 1); + New_Line; + Disp_Tree (Get_Right (N), Indent + 1, Full); + null; + when N_Braced_SERE => + if not Full then + return; + end if; + Disp_Header ("SERE", Indent + 1); + New_Line; + Disp_Tree (Get_SERE (N), Indent + 1, Full); + null; + when N_Concat_SERE => + if not Full then + return; + end if; + Disp_Header ("Left", Indent + 1); + New_Line; + Disp_Tree (Get_Left (N), Indent + 1, Full); + Disp_Header ("Right", Indent + 1); + New_Line; + Disp_Tree (Get_Right (N), Indent + 1, Full); + null; + when N_Fusion_SERE => + if not Full then + return; + end if; + Disp_Header ("Left", Indent + 1); + New_Line; + Disp_Tree (Get_Left (N), Indent + 1, Full); + Disp_Header ("Right", Indent + 1); + New_Line; + Disp_Tree (Get_Right (N), Indent + 1, Full); + null; + when N_Within_SERE => + if not Full then + return; + end if; + Disp_Header ("Left", Indent + 1); + New_Line; + Disp_Tree (Get_Left (N), Indent + 1, Full); + Disp_Header ("Right", Indent + 1); + New_Line; + Disp_Tree (Get_Right (N), Indent + 1, Full); + null; + when N_Match_And_Seq => + if not Full then + return; + end if; + Disp_Header ("Left", Indent + 1); + New_Line; + Disp_Tree (Get_Left (N), Indent + 1, Full); + Disp_Header ("Right", Indent + 1); + New_Line; + Disp_Tree (Get_Right (N), Indent + 1, Full); + null; + when N_And_Seq => + if not Full then + return; + end if; + Disp_Header ("Left", Indent + 1); + New_Line; + Disp_Tree (Get_Left (N), Indent + 1, Full); + Disp_Header ("Right", Indent + 1); + New_Line; + Disp_Tree (Get_Right (N), Indent + 1, Full); + null; + when N_Or_Seq => + if not Full then + return; + end if; + Disp_Header ("Left", Indent + 1); + New_Line; + Disp_Tree (Get_Left (N), Indent + 1, Full); + Disp_Header ("Right", Indent + 1); + New_Line; + Disp_Tree (Get_Right (N), Indent + 1, Full); + null; + when N_Star_Repeat_Seq => + if not Full then + return; + end if; + Disp_Header ("Sequence", Indent + 1); + New_Line; + Disp_Tree (Get_Sequence (N), Indent + 1, Full); + Disp_Header ("Low_Bound", Indent + 1); + New_Line; + Disp_Tree (Get_Low_Bound (N), Indent + 1, Full); + Disp_Header ("High_Bound", Indent + 1); + New_Line; + Disp_Tree (Get_High_Bound (N), Indent + 1, Full); + null; + when N_Goto_Repeat_Seq => + if not Full then + return; + end if; + Disp_Header ("Sequence", Indent + 1); + New_Line; + Disp_Tree (Get_Sequence (N), Indent + 1, Full); + Disp_Header ("Low_Bound", Indent + 1); + New_Line; + Disp_Tree (Get_Low_Bound (N), Indent + 1, Full); + Disp_Header ("High_Bound", Indent + 1); + New_Line; + Disp_Tree (Get_High_Bound (N), Indent + 1, Full); + null; + when N_Plus_Repeat_Seq => + if not Full then + return; + end if; + Disp_Header ("Sequence", Indent + 1); + New_Line; + Disp_Tree (Get_Sequence (N), Indent + 1, Full); + null; + when N_Equal_Repeat_Seq => + if not Full then + return; + end if; + Disp_Header ("Sequence", Indent + 1); + New_Line; + Disp_Tree (Get_Sequence (N), Indent + 1, Full); + Disp_Header ("Low_Bound", Indent + 1); + New_Line; + Disp_Tree (Get_Low_Bound (N), Indent + 1, Full); + Disp_Header ("High_Bound", Indent + 1); + New_Line; + Disp_Tree (Get_High_Bound (N), Indent + 1, Full); + null; + when N_Not_Bool => + if not Full then + return; + end if; + Disp_Header ("Boolean", Indent + 1); + New_Line; + Disp_Tree (Get_Boolean (N), Indent + 1, Full); + Disp_Header ("Presence", Indent + 1); + Disp_PSL_Presence_Kind (Get_Presence (N)); + New_Line; + Disp_Header ("Hash", Indent + 1); + Disp_Uns32 (Get_Hash (N)); + New_Line; + Disp_Header ("Hash_Link", Indent + 1); + New_Line; + Disp_Tree (Get_Hash_Link (N), Indent + 1, Full); + null; + when N_And_Bool => + if not Full then + return; + end if; + Disp_Header ("Left", Indent + 1); + New_Line; + Disp_Tree (Get_Left (N), Indent + 1, Full); + Disp_Header ("Right", Indent + 1); + New_Line; + Disp_Tree (Get_Right (N), Indent + 1, Full); + Disp_Header ("Presence", Indent + 1); + Disp_PSL_Presence_Kind (Get_Presence (N)); + New_Line; + Disp_Header ("Hash", Indent + 1); + Disp_Uns32 (Get_Hash (N)); + New_Line; + Disp_Header ("Hash_Link", Indent + 1); + New_Line; + Disp_Tree (Get_Hash_Link (N), Indent + 1, Full); + null; + when N_Or_Bool => + if not Full then + return; + end if; + Disp_Header ("Left", Indent + 1); + New_Line; + Disp_Tree (Get_Left (N), Indent + 1, Full); + Disp_Header ("Right", Indent + 1); + New_Line; + Disp_Tree (Get_Right (N), Indent + 1, Full); + Disp_Header ("Presence", Indent + 1); + Disp_PSL_Presence_Kind (Get_Presence (N)); + New_Line; + Disp_Header ("Hash", Indent + 1); + Disp_Uns32 (Get_Hash (N)); + New_Line; + Disp_Header ("Hash_Link", Indent + 1); + New_Line; + Disp_Tree (Get_Hash_Link (N), Indent + 1, Full); + null; + when N_Imp_Bool => + if not Full then + return; + end if; + Disp_Header ("Left", Indent + 1); + New_Line; + Disp_Tree (Get_Left (N), Indent + 1, Full); + Disp_Header ("Right", Indent + 1); + New_Line; + Disp_Tree (Get_Right (N), Indent + 1, Full); + Disp_Header ("Presence", Indent + 1); + Disp_PSL_Presence_Kind (Get_Presence (N)); + New_Line; + Disp_Header ("Hash", Indent + 1); + Disp_Uns32 (Get_Hash (N)); + New_Line; + Disp_Header ("Hash_Link", Indent + 1); + New_Line; + Disp_Tree (Get_Hash_Link (N), Indent + 1, Full); + null; + when N_HDL_Expr => + if not Full then + return; + end if; + Disp_Header ("Presence", Indent + 1); + Disp_PSL_Presence_Kind (Get_Presence (N)); + New_Line; + Disp_Header ("HDL_Node", Indent + 1); + Disp_HDL_Node (Get_HDL_Node (N)); + New_Line; + Disp_Header ("HDL_Index", Indent + 1); + Disp_Int32 (Get_HDL_Index (N)); + New_Line; + Disp_Header ("Hash", Indent + 1); + Disp_Uns32 (Get_Hash (N)); + New_Line; + Disp_Header ("Hash_Link", Indent + 1); + New_Line; + Disp_Tree (Get_Hash_Link (N), Indent + 1, Full); + null; + when N_False => + if not Full then + return; + end if; + null; + when N_True => + if not Full then + return; + end if; + null; + when N_EOS => + if not Full then + return; + end if; + Disp_Header ("HDL_Index", Indent + 1); + Disp_Int32 (Get_HDL_Index (N)); + New_Line; + Disp_Header ("Hash", Indent + 1); + Disp_Uns32 (Get_Hash (N)); + New_Line; + Disp_Header ("Hash_Link", Indent + 1); + New_Line; + Disp_Tree (Get_Hash_Link (N), Indent + 1, Full); + null; + when N_Name => + Disp_Header ("Identifier", Indent + 1); + Disp_Identifier (N); + if not Full then + return; + end if; + Disp_Header ("Decl", Indent + 1); + New_Line; + Disp_Tree (Get_Decl (N), Indent + 1, Full); + null; + when N_Name_Decl => + Disp_Header ("Identifier", Indent + 1); + Disp_Identifier (N); + if not Full then + return; + end if; + Disp_Tree (Get_Chain (N), Indent, Full); + null; + when N_Number => + if not Full then + return; + end if; + Disp_Header ("Value", Indent + 1); + Disp_Uns32 (Get_Value (N)); + New_Line; + null; + end case; + end Disp_Tree; + + procedure Dump_Tree (N : Node; Full : Boolean := False) is + begin + Disp_Tree (N, 0, Full); + end Dump_Tree; + +end PSL.Dump_Tree; diff --git a/src/psl/psl-dump_tree.ads b/src/psl/psl-dump_tree.ads new file mode 100644 index 000000000..f8b2eb3ab --- /dev/null +++ b/src/psl/psl-dump_tree.ads @@ -0,0 +1,9 @@ +with PSL.Nodes; use PSL.Nodes; + +package PSL.Dump_Tree is + procedure Dump_Tree (N : Node; Full : Boolean := False); + + -- Procedure to dump an HDL node. + type Dump_Hdl_Node_Acc is access procedure (N : HDL_Node); + Dump_Hdl_Node : Dump_Hdl_Node_Acc := null; +end PSL.Dump_Tree; diff --git a/src/psl/psl-hash.adb b/src/psl/psl-hash.adb new file mode 100644 index 000000000..62744b336 --- /dev/null +++ b/src/psl/psl-hash.adb @@ -0,0 +1,60 @@ +with GNAT.Table; + +package body PSL.Hash is + + type Index_Type is new Natural; + No_Index : constant Index_Type := 0; + + type Cell_Record is record + Res : Node; + Next : Index_Type; + end record; + + Hash_Size : constant Index_Type := 127; + + package Cells is new GNAT.Table + (Table_Component_Type => Cell_Record, + Table_Index_Type => Index_Type, + Table_Low_Bound => 0, + Table_Initial => 256, + Table_Increment => 100); + + procedure Init is + begin + Cells.Set_Last (Hash_Size - 1); + for I in 0 .. Hash_Size - 1 loop + Cells.Table (I) := (Res => Null_Node, Next => No_Index); + end loop; + end Init; + + function Get_PSL_Node (Hdl : Int32) return Node is + Idx : Index_Type := Index_Type (Hdl mod Int32 (Hash_Size)); + N_Idx : Index_Type; + Res : Node; + begin + -- In the primary table. + Res := Cells.Table (Idx).Res; + if Res = Null_Node then + Res := Create_Node (N_HDL_Expr); + Set_HDL_Node (Res, Hdl); + Cells.Table (Idx).Res := Res; + return Res; + end if; + + loop + if Get_HDL_Node (Res) = Hdl then + return Res; + end if; + -- Look in collisions chain + N_Idx := Cells.Table (Idx).Next; + exit when N_Idx = No_Index; + Idx := N_Idx; + Res := Cells.Table (Idx).Res; + end loop; + Res := Create_Node (N_HDL_Expr); + Set_HDL_Node (Res, Hdl); + Cells.Append ((Res => Res, Next => No_Index)); + Cells.Table (Idx).Next := Cells.Last; + return Res; + end Get_PSL_Node; +end PSL.Hash; diff --git a/src/psl/psl-hash.ads b/src/psl/psl-hash.ads new file mode 100644 index 000000000..d1a60c971 --- /dev/null +++ b/src/psl/psl-hash.ads @@ -0,0 +1,11 @@ +with Types; use Types; +with PSL.Nodes; use PSL.Nodes; + +package PSL.Hash is + -- Initialize the package. + procedure Init; + + -- Get the PSL node for node HDL. + -- Only one PSL node is created for an HDL node. + function Get_PSL_Node (Hdl : Int32) return Node; +end PSL.Hash; diff --git a/src/psl/psl-nfas-utils.adb b/src/psl/psl-nfas-utils.adb new file mode 100644 index 000000000..06601850d --- /dev/null +++ b/src/psl/psl-nfas-utils.adb @@ -0,0 +1,330 @@ +with PSL.Errors; use PSL.Errors; + +package body PSL.NFAs.Utils is + generic + with function Get_First_Edge (S : NFA_State) return NFA_Edge; + with function Get_Next_Edge (E : NFA_Edge) return NFA_Edge; + with procedure Set_First_Edge (S : NFA_State; E : NFA_Edge); + with procedure Set_Next_Edge (E : NFA_Edge; N_E : NFA_Edge); + with function Get_Edge_State (E : NFA_Edge) return NFA_State; + package Sort_Edges is + procedure Sort_Edges (S : NFA_State); + procedure Sort_Edges (N : NFA); + end Sort_Edges; + + package body Sort_Edges is + -- Use merge sort to sort a list of edges. + -- The first edge is START and the list has LEN edges. + -- RES is the head of the sorted list. + -- NEXT_EDGE is the LEN + 1 edge (not sorted). + procedure Edges_Merge_Sort (Start : NFA_Edge; + Len : Natural; + Res : out NFA_Edge; + Next_Edge : out NFA_Edge) + is + function Lt (L, R : NFA_Edge) return Boolean + is + L_Expr : constant Node := Get_Edge_Expr (L); + R_Expr : constant Node := Get_Edge_Expr (R); + begin + return L_Expr < R_Expr + or else (L_Expr = R_Expr + and then Get_Edge_State (L) < Get_Edge_State (R)); + end Lt; + + pragma Inline (Lt); + + Half : constant Natural := Len / 2; + Left_Start, Right_Start : NFA_Edge; + Left_Next, Right_Next : NFA_Edge; + L, R : NFA_Edge; + Last, E : NFA_Edge; + begin + -- With less than 2 elements, the sort is trivial. + if Len < 2 then + if Len = 0 then + Next_Edge := Start; + else + Next_Edge := Get_Next_Edge (Start); + end if; + Res := Start; + return; + end if; + + -- Sort each half. + Edges_Merge_Sort (Start, Half, Left_Start, Left_Next); + Edges_Merge_Sort (Left_Next, Len - Half, Right_Start, Right_Next); + + -- Merge. + L := Left_Start; + R := Right_Start; + Last := No_Edge; + loop + -- Take from left iff: + -- * it is not empty + -- * right is empty or else (left < right) + if L /= Left_Next and then (R = Right_Next or else Lt (L, R)) then + E := L; + L := Get_Next_Edge (L); + + -- Take from right if right is not empty. + elsif R /= Right_Next then + E := R; + R := Get_Next_Edge (R); + + -- Both left are right are empty. + else + exit; + end if; + + if Last = No_Edge then + Res := E; + else + Set_Next_Edge (Last, E); + end if; + Last := E; + end loop; + -- Let the link clean. + Next_Edge := Right_Next; + Set_Next_Edge (Last, Next_Edge); + end Edges_Merge_Sort; + + procedure Sort_Edges (S : NFA_State) + is + Nbr_Edges : Natural; + First_E, E, Res : NFA_Edge; + begin + -- Count number of edges. + Nbr_Edges := 0; + First_E := Get_First_Edge (S); + E := First_E; + while E /= No_Edge loop + Nbr_Edges := Nbr_Edges + 1; + E := Get_Next_Edge (E); + end loop; + + -- Sort edges by expression. + Edges_Merge_Sort (First_E, Nbr_Edges, Res, E); + pragma Assert (E = No_Edge); + Set_First_Edge (S, Res); + + end Sort_Edges; + + procedure Sort_Edges (N : NFA) + is + S : NFA_State; + begin + -- Iterate on states. + S := Get_First_State (N); + while S /= No_State loop + Sort_Edges (S); + S := Get_Next_State (S); + end loop; + end Sort_Edges; + end Sort_Edges; + + package Sort_Src_Edges_Pkg is new + Sort_Edges (Get_First_Edge => Get_First_Src_Edge, + Get_Next_Edge => Get_Next_Src_Edge, + Set_First_Edge => Set_First_Src_Edge, + Set_Next_Edge => Set_Next_Src_Edge, + Get_Edge_State => Get_Edge_Dest); + + procedure Sort_Src_Edges (S : NFA_State) renames + Sort_Src_Edges_Pkg.Sort_Edges; + procedure Sort_Src_Edges (N : NFA) renames + Sort_Src_Edges_Pkg.Sort_Edges; + + package Sort_Dest_Edges_Pkg is new + Sort_Edges (Get_First_Edge => Get_First_Dest_Edge, + Get_Next_Edge => Get_Next_Dest_Edge, + Set_First_Edge => Set_First_Dest_Edge, + Set_Next_Edge => Set_Next_Dest_Edge, + Get_Edge_State => Get_Edge_Src); + + procedure Sort_Dest_Edges (S : NFA_State) renames + Sort_Dest_Edges_Pkg.Sort_Edges; + procedure Sort_Dest_Edges (N : NFA) renames + Sort_Dest_Edges_Pkg.Sort_Edges; + + generic + with function Get_First_Edge_Reverse (S : NFA_State) return NFA_Edge; + with function Get_First_Edge (S : NFA_State) return NFA_Edge; + with procedure Set_First_Edge (S : NFA_State; E : NFA_Edge); + with function Get_Next_Edge (E : NFA_Edge) return NFA_Edge; + with procedure Set_Next_Edge (E : NFA_Edge; E1 : NFA_Edge); + with procedure Set_Edge_State (E : NFA_Edge; S : NFA_State); + procedure Merge_State (N : NFA; S : NFA_State; S1 : NFA_State); + + procedure Merge_State (N : NFA; S : NFA_State; S1 : NFA_State) + is + E, First_E, Next_E : NFA_Edge; + begin + pragma Assert (S /= S1); + + -- Discard outgoing edges of S1. + loop + E := Get_First_Edge_Reverse (S1); + exit when E = No_Edge; + Remove_Edge (E); + end loop; + + -- Prepend incoming edges of S1 to S. + First_E := Get_First_Edge (S); + E := Get_First_Edge (S1); + while E /= No_Edge loop + Next_E := Get_Next_Edge (E); + Set_Next_Edge (E, First_E); + Set_Edge_State (E, S); + First_E := E; + E := Next_E; + end loop; + Set_First_Edge (S, First_E); + Set_First_Edge (S1, No_Edge); + + Remove_State (N, S1); + end Merge_State; + + procedure Merge_State_Dest_1 is new Merge_State + (Get_First_Edge_Reverse => Get_First_Src_Edge, + Get_First_Edge => Get_First_Dest_Edge, + Set_First_Edge => Set_First_Dest_Edge, + Get_Next_Edge => Get_Next_Dest_Edge, + Set_Next_Edge => Set_Next_Dest_Edge, + Set_Edge_State => Set_Edge_Dest); + + procedure Merge_State_Dest (N : NFA; S : NFA_State; S1 : NFA_State) renames + Merge_State_Dest_1; + + procedure Merge_State_Src_1 is new Merge_State + (Get_First_Edge_Reverse => Get_First_Dest_Edge, + Get_First_Edge => Get_First_Src_Edge, + Set_First_Edge => Set_First_Src_Edge, + Get_Next_Edge => Get_Next_Src_Edge, + Set_Next_Edge => Set_Next_Src_Edge, + Set_Edge_State => Set_Edge_Src); + + procedure Merge_State_Src (N : NFA; S : NFA_State; S1 : NFA_State) renames + Merge_State_Src_1; + + procedure Sort_Outgoing_Edges (N : NFA; Nbr_States : Natural) + is + Last_State : constant NFA_State := NFA_State (Nbr_States) - 1; + type Edge_Array is array (0 .. Last_State) of NFA_Edge; + Edges : Edge_Array := (others => No_Edge); + S, D : NFA_State; + E, Next_E : NFA_Edge; + First_Edge, Last_Edge : NFA_Edge; + begin + -- Iterate on states. + S := Get_First_State (N); + while S /= No_State loop + + -- Create an array of edges + E := Get_First_Dest_Edge (S); + while E /= No_Edge loop + Next_E := Get_Next_Dest_Edge (E); + D := Get_Edge_Dest (E); + if Edges (D) /= No_Edge then + -- TODO: merge edges. + raise Program_Error; + end if; + Edges (D) := E; + E := Next_E; + end loop; + + -- Rebuild the edge list (sorted by destination). + Last_Edge := No_Edge; + First_Edge := No_Edge; + for I in Edge_Array'Range loop + E := Edges (I); + if E /= No_Edge then + Edges (I) := No_Edge; + if First_Edge = No_Edge then + First_Edge := E; + else + Set_Next_Dest_Edge (Last_Edge, E); + end if; + Last_Edge := E; + end if; + end loop; + Set_First_Dest_Edge (S, First_Edge); + S := Get_Next_State (S); + end loop; + end Sort_Outgoing_Edges; + pragma Unreferenced (Sort_Outgoing_Edges); + + generic + with function Get_First_Edge (S : NFA_State) return NFA_Edge; + with function Get_Next_Edge (E : NFA_Edge) return NFA_Edge; + with function Get_State_Reverse (E : NFA_Edge) return NFA_State; + with function Get_First_Edge_Reverse (S : NFA_State) return NFA_Edge; + with function Get_Next_Edge_Reverse (E : NFA_Edge) return NFA_Edge; + procedure Check_Edges_Gen (N : NFA); + + procedure Check_Edges_Gen (N : NFA) + is + S : NFA_State; + E : NFA_Edge; + R_S : NFA_State; + R_E : NFA_Edge; + begin + S := Get_First_State (N); + while S /= No_State loop + E := Get_First_Edge (S); + while E /= No_Edge loop + R_S := Get_State_Reverse (E); + R_E := Get_First_Edge_Reverse (R_S); + while R_E /= No_Edge and then R_E /= E loop + R_E := Get_Next_Edge_Reverse (R_E); + end loop; + if R_E /= E then + raise Program_Error; + end if; + E := Get_Next_Edge (E); + end loop; + S := Get_Next_State (S); + end loop; + end Check_Edges_Gen; + + procedure Check_Edges_Src is new Check_Edges_Gen + (Get_First_Edge => Get_First_Src_Edge, + Get_Next_Edge => Get_Next_Src_Edge, + Get_State_Reverse => Get_Edge_Dest, + Get_First_Edge_Reverse => Get_First_Dest_Edge, + Get_Next_Edge_Reverse => Get_Next_Dest_Edge); + + procedure Check_Edges_Dest is new Check_Edges_Gen + (Get_First_Edge => Get_First_Dest_Edge, + Get_Next_Edge => Get_Next_Dest_Edge, + Get_State_Reverse => Get_Edge_Src, + Get_First_Edge_Reverse => Get_First_Src_Edge, + Get_Next_Edge_Reverse => Get_Next_Src_Edge); + + procedure Check_NFA (N : NFA) is + begin + Check_Edges_Src (N); + Check_Edges_Dest (N); + end Check_NFA; + + function Has_EOS (N : Node) return Boolean is + begin + case Get_Kind (N) is + when N_EOS => + return True; + when N_False + | N_True + | N_HDL_Expr => + return False; + when N_Not_Bool => + return Has_EOS (Get_Boolean (N)); + when N_And_Bool + | N_Or_Bool + | N_Imp_Bool => + return Has_EOS (Get_Left (N)) or else Has_EOS (Get_Right (N)); + when others => + Error_Kind ("Has_EOS", N); + end case; + end Has_EOS; + +end PSL.NFAs.Utils; diff --git a/src/psl/psl-nfas-utils.ads b/src/psl/psl-nfas-utils.ads new file mode 100644 index 000000000..bdbc0d013 --- /dev/null +++ b/src/psl/psl-nfas-utils.ads @@ -0,0 +1,21 @@ +package PSL.NFAs.Utils is + -- Sort outgoing edges by expression. + procedure Sort_Src_Edges (S : NFA_State); + procedure Sort_Src_Edges (N : NFA); + + procedure Sort_Dest_Edges (S : NFA_State); + procedure Sort_Dest_Edges (N : NFA); + + -- Move incoming edges of S1 to S, remove S1 and its outgoing edges. + procedure Merge_State_Dest (N : NFA; S : NFA_State; S1 : NFA_State); + + procedure Merge_State_Src (N : NFA; S : NFA_State; S1 : NFA_State); + + -- Return True if N or a child of N is EOS. + -- N must be a boolean expression. + function Has_EOS (N : Node) return Boolean; + + -- Raise Program_Error if N is not internally coherent. + procedure Check_NFA (N : NFA); +end PSL.NFAs.Utils; + diff --git a/src/psl/psl-nfas.adb b/src/psl/psl-nfas.adb new file mode 100644 index 000000000..da4866e53 --- /dev/null +++ b/src/psl/psl-nfas.adb @@ -0,0 +1,529 @@ +with GNAT.Table; + +package body PSL.NFAs is + -- Record that describes an NFA. + type NFA_Node is record + -- Chain of States. + First_State : NFA_State; + Last_State : NFA_State; + + -- Start and final state. + Start : NFA_State; + Final : NFA_State; + + -- If true there is an epsilon transition between the start and + -- the final state. + Epsilon : Boolean; + end record; + + -- Record that describe a node. + type NFA_State_Node is record + -- States may be numbered. + Label : Int32; + + -- Edges. + First_Src : NFA_Edge; + First_Dst : NFA_Edge; + + -- State links. + Next_State : NFA_State; + Prev_State : NFA_State; + + -- User fields. + User_Link : NFA_State; + User_Flag : Boolean; + end record; + + -- Record that describe an edge between SRC and DEST. + type NFA_Edge_Node is record + Dest : NFA_State; + Src : NFA_State; + Expr : Node; + + -- Links. + Next_Src : NFA_Edge; + Next_Dst : NFA_Edge; + end record; + + -- Table of NFA. + package Nfat is new GNAT.Table + (Table_Component_Type => NFA_Node, + Table_Index_Type => NFA, + Table_Low_Bound => 1, + Table_Initial => 128, + Table_Increment => 100); + + -- List of free nodes. + Free_Nfas : NFA := No_NFA; + + -- Table of States. + package Statet is new GNAT.Table + (Table_Component_Type => NFA_State_Node, + Table_Index_Type => NFA_State, + Table_Low_Bound => 1, + Table_Initial => 128, + Table_Increment => 100); + + -- List of free states. + Free_States : NFA_State := No_State; + + -- Table of edges. + package Transt is new GNAT.Table + (Table_Component_Type => NFA_Edge_Node, + Table_Index_Type => NFA_Edge, + Table_Low_Bound => 1, + Table_Initial => 128, + Table_Increment => 100); + + -- List of free edges. + Free_Edges : NFA_Edge := No_Edge; + + function Get_First_State (N : NFA) return NFA_State is + begin + return Nfat.Table (N).First_State; + end Get_First_State; + + function Get_Last_State (N : NFA) return NFA_State is + begin + return Nfat.Table (N).Last_State; + end Get_Last_State; + + procedure Set_First_State (N : NFA; S : NFA_State) is + begin + Nfat.Table (N).First_State := S; + end Set_First_State; + + procedure Set_Last_State (N : NFA; S : NFA_State) is + begin + Nfat.Table (N).Last_State := S; + end Set_Last_State; + + function Get_Next_State (S : NFA_State) return NFA_State is + begin + return Statet.Table (S).Next_State; + end Get_Next_State; + + procedure Set_Next_State (S : NFA_State; N : NFA_State) is + begin + Statet.Table (S).Next_State := N; + end Set_Next_State; + + function Get_Prev_State (S : NFA_State) return NFA_State is + begin + return Statet.Table (S).Prev_State; + end Get_Prev_State; + + procedure Set_Prev_State (S : NFA_State; N : NFA_State) is + begin + Statet.Table (S).Prev_State := N; + end Set_Prev_State; + + function Get_State_Label (S : NFA_State) return Int32 is + begin + return Statet.Table (S).Label; + end Get_State_Label; + + procedure Set_State_Label (S : NFA_State; Label : Int32) is + begin + Statet.Table (S).Label := Label; + end Set_State_Label; + + function Get_Epsilon_NFA (N : NFA) return Boolean is + begin + return Nfat.Table (N).Epsilon; + end Get_Epsilon_NFA; + + procedure Set_Epsilon_NFA (N : NFA; Flag : Boolean) is + begin + Nfat.Table (N).Epsilon := Flag; + end Set_Epsilon_NFA; + + function Add_State (N : NFA) return NFA_State is + Res : NFA_State; + Last : NFA_State; + begin + -- Get a new state. + if Free_States = No_State then + Statet.Increment_Last; + Res := Statet.Last; + else + Res := Free_States; + Free_States := Get_Next_State (Res); + end if; + + -- Put it in N. + Last := Get_Last_State (N); + Statet.Table (Res) := (Label => 0, + First_Src => No_Edge, + First_Dst => No_Edge, + Next_State => No_State, + Prev_State => Last, + User_Link => No_State, + User_Flag => False); + if Last = No_State then + Nfat.Table (N).First_State := Res; + else + Statet.Table (Last).Next_State := Res; + end if; + Nfat.Table (N).Last_State := Res; + return Res; + end Add_State; + + procedure Delete_Detached_State (S : NFA_State) is + begin + -- Put it in front of the free_states list. + Set_Next_State (S, Free_States); + Free_States := S; + end Delete_Detached_State; + + function Create_NFA return NFA + is + Res : NFA; + begin + -- Allocate a node. + if Free_Nfas = No_NFA then + Nfat.Increment_Last; + Res := Nfat.Last; + else + Res := Free_Nfas; + Free_Nfas := NFA (Get_First_State (Res)); + end if; + + -- Fill it. + Nfat.Table (Res) := (First_State => No_State, + Last_State => No_State, + Start => No_State, Final => No_State, + Epsilon => False); + return Res; + end Create_NFA; + + procedure Set_First_Src_Edge (N : NFA_State; T : NFA_Edge) is + begin + Statet.Table (N).First_Src := T; + end Set_First_Src_Edge; + + function Get_First_Src_Edge (N : NFA_State) return NFA_Edge is + begin + return Statet.Table (N).First_Src; + end Get_First_Src_Edge; + + procedure Set_First_Dest_Edge (N : NFA_State; T : NFA_Edge) is + begin + Statet.Table (N).First_Dst := T; + end Set_First_Dest_Edge; + + function Get_First_Dest_Edge (N : NFA_State) return NFA_Edge is + begin + return Statet.Table (N).First_Dst; + end Get_First_Dest_Edge; + + function Get_State_Flag (S : NFA_State) return Boolean is + begin + return Statet.Table (S).User_Flag; + end Get_State_Flag; + + procedure Set_State_Flag (S : NFA_State; Val : Boolean) is + begin + Statet.Table (S).User_Flag := Val; + end Set_State_Flag; + + function Get_State_User_Link (S : NFA_State) return NFA_State is + begin + return Statet.Table (S).User_Link; + end Get_State_User_Link; + + procedure Set_State_User_Link (S : NFA_State; Link : NFA_State) is + begin + Statet.Table (S).User_Link := Link; + end Set_State_User_Link; + + function Add_Edge (Src : NFA_State; Dest : NFA_State; Expr : Node) + return NFA_Edge + is + Res : NFA_Edge; + begin + -- Allocate a note. + if Free_Edges /= No_Edge then + Res := Free_Edges; + Free_Edges := Get_Next_Dest_Edge (Res); + else + Transt.Increment_Last; + Res := Transt.Last; + end if; + + -- Initialize it. + Transt.Table (Res) := (Dest => Dest, + Src => Src, + Expr => Expr, + Next_Src => Get_First_Src_Edge (Src), + Next_Dst => Get_First_Dest_Edge (Dest)); + Set_First_Src_Edge (Src, Res); + Set_First_Dest_Edge (Dest, Res); + return Res; + end Add_Edge; + + procedure Add_Edge (Src : NFA_State; Dest : NFA_State; Expr : Node) is + Res : NFA_Edge; + pragma Unreferenced (Res); + begin + Res := Add_Edge (Src, Dest, Expr); + end Add_Edge; + + procedure Delete_Empty_NFA (N : NFA) is + begin + pragma Assert (Get_First_State (N) = No_State); + pragma Assert (Get_Last_State (N) = No_State); + + -- Put it in front of the free_nfas list. + Set_First_State (N, NFA_State (Free_Nfas)); + Free_Nfas := N; + end Delete_Empty_NFA; + + function Get_Start_State (N : NFA) return NFA_State is + begin + return Nfat.Table (N).Start; + end Get_Start_State; + + procedure Set_Start_State (N : NFA; S : NFA_State) is + begin + Nfat.Table (N).Start := S; + end Set_Start_State; + + function Get_Final_State (N : NFA) return NFA_State is + begin + return Nfat.Table (N).Final; + end Get_Final_State; + + procedure Set_Final_State (N : NFA; S : NFA_State) is + begin + Nfat.Table (N).Final := S; + end Set_Final_State; + + function Get_Next_Src_Edge (N : NFA_Edge) return NFA_Edge is + begin + return Transt.Table (N).Next_Src; + end Get_Next_Src_Edge; + + procedure Set_Next_Src_Edge (E : NFA_Edge; N_E : NFA_Edge) is + begin + Transt.Table (E).Next_Src := N_E; + end Set_Next_Src_Edge; + + function Get_Next_Dest_Edge (N : NFA_Edge) return NFA_Edge is + begin + return Transt.Table (N).Next_Dst; + end Get_Next_Dest_Edge; + + procedure Set_Next_Dest_Edge (E : NFA_Edge; N_E : NFA_Edge) is + begin + Transt.Table (E).Next_Dst := N_E; + end Set_Next_Dest_Edge; + + function Get_Edge_Dest (E : NFA_Edge) return NFA_State is + begin + return Transt.Table (E).Dest; + end Get_Edge_Dest; + + procedure Set_Edge_Dest (E : NFA_Edge; D : NFA_State) is + begin + Transt.Table (E).Dest := D; + end Set_Edge_Dest; + + function Get_Edge_Src (E : NFA_Edge) return NFA_State is + begin + return Transt.Table (E).Src; + end Get_Edge_Src; + + procedure Set_Edge_Src (E : NFA_Edge; D : NFA_State) is + begin + Transt.Table (E).Src := D; + end Set_Edge_Src; + + function Get_Edge_Expr (E : NFA_Edge) return Node is + begin + return Transt.Table (E).Expr; + end Get_Edge_Expr; + + procedure Set_Edge_Expr (E : NFA_Edge; N : Node) is + begin + Transt.Table (E).Expr := N; + end Set_Edge_Expr; + + procedure Remove_Unconnected_State (N : NFA; S : NFA_State) is + N_S : constant NFA_State := Get_Next_State (S); + P_S : constant NFA_State := Get_Prev_State (S); + begin + pragma Assert (Get_First_Src_Edge (S) = No_Edge); + pragma Assert (Get_First_Dest_Edge (S) = No_Edge); + + if P_S = No_State then + Set_First_State (N, N_S); + else + Set_Next_State (P_S, N_S); + end if; + if N_S = No_State then + Set_Last_State (N, P_S); + else + Set_Prev_State (N_S, P_S); + end if; + Delete_Detached_State (S); + end Remove_Unconnected_State; + + procedure Merge_NFA (L, R : NFA) is + Last_L : constant NFA_State := Get_Last_State (L); + First_R : constant NFA_State := Get_First_State (R); + Last_R : constant NFA_State := Get_Last_State (R); + begin + if First_R = No_State then + return; + end if; + if Last_L = No_State then + Set_First_State (L, First_R); + else + Set_Next_State (Last_L, First_R); + Set_Prev_State (First_R, Last_L); + end if; + Set_Last_State (L, Last_R); + Set_First_State (R, No_State); + Set_Last_State (R, No_State); + Delete_Empty_NFA (R); + end Merge_NFA; + + procedure Redest_Edges (S : NFA_State; Dest : NFA_State) is + E, N_E : NFA_Edge; + Head : NFA_Edge; + begin + E := Get_First_Dest_Edge (S); + if E = No_Edge then + return; + end if; + Set_First_Dest_Edge (S, No_Edge); + Head := Get_First_Dest_Edge (Dest); + Set_First_Dest_Edge (Dest, E); + loop + N_E := Get_Next_Dest_Edge (E); + Set_Edge_Dest (E, Dest); + exit when N_E = No_Edge; + E := N_E; + end loop; + Set_Next_Dest_Edge (E, Head); + end Redest_Edges; + + procedure Resource_Edges (S : NFA_State; Src : NFA_State) is + E, N_E : NFA_Edge; + Head : NFA_Edge; + begin + E := Get_First_Src_Edge (S); + if E = No_Edge then + return; + end if; + Set_First_Src_Edge (S, No_Edge); + Head := Get_First_Src_Edge (Src); + Set_First_Src_Edge (Src, E); + loop + N_E := Get_Next_Src_Edge (E); + Set_Edge_Src (E, Src); + exit when N_E = No_Edge; + E := N_E; + end loop; + Set_Next_Src_Edge (E, Head); + end Resource_Edges; + + procedure Disconnect_Edge_Src (N : NFA_State; E : NFA_Edge) is + N_E : constant NFA_Edge := Get_Next_Src_Edge (E); + Prev, Cur : NFA_Edge; + begin + Cur := Get_First_Src_Edge (N); + if Cur = E then + Set_First_Src_Edge (N, N_E); + else + while Cur /= E loop + Prev := Cur; + Cur := Get_Next_Src_Edge (Prev); + pragma Assert (Cur /= No_Edge); + end loop; + Set_Next_Src_Edge (Prev, N_E); + end if; + end Disconnect_Edge_Src; + + procedure Disconnect_Edge_Dest (N : NFA_State; E : NFA_Edge) is + N_E : constant NFA_Edge := Get_Next_Dest_Edge (E); + Prev, Cur : NFA_Edge; + begin + Cur := Get_First_Dest_Edge (N); + if Cur = E then + Set_First_Dest_Edge (N, N_E); + else + while Cur /= E loop + Prev := Cur; + Cur := Get_Next_Dest_Edge (Prev); + pragma Assert (Cur /= No_Edge); + end loop; + Set_Next_Dest_Edge (Prev, N_E); + end if; + end Disconnect_Edge_Dest; + + procedure Remove_Edge (E : NFA_Edge) is + begin + Disconnect_Edge_Src (Get_Edge_Src (E), E); + Disconnect_Edge_Dest (Get_Edge_Dest (E), E); + + -- Put it on the free list. + Set_Next_Dest_Edge (E, Free_Edges); + Free_Edges := E; + end Remove_Edge; + + procedure Remove_State (N : NFA; S : NFA_State) is + E, N_E : NFA_Edge; + begin + E := Get_First_Dest_Edge (S); + while E /= No_Edge loop + N_E := Get_Next_Dest_Edge (E); + Remove_Edge (E); + E := N_E; + end loop; + + E := Get_First_Src_Edge (S); + while E /= No_Edge loop + N_E := Get_Next_Src_Edge (E); + Remove_Edge (E); + E := N_E; + end loop; + + Remove_Unconnected_State (N, S); + end Remove_State; + + procedure Labelize_States (N : NFA; Nbr_States : out Natural) + is + S, Start, Final : NFA_State; + begin + S := Get_First_State (N); + Start := Get_Start_State (N); + Final := Get_Final_State (N); + pragma Assert (Start /= No_State); + Set_State_Label (Start, 0); + Nbr_States := 1; + while S /= No_State loop + if S /= Start and then S /= Final then + Set_State_Label (S, Int32 (Nbr_States)); + Nbr_States := Nbr_States + 1; + end if; + S := Get_Next_State (S); + end loop; + pragma Assert (Final /= No_State); + Set_State_Label (Final, Int32 (Nbr_States)); + Nbr_States := Nbr_States + 1; + end Labelize_States; + + procedure Labelize_States_Debug (N : NFA) + is + S : NFA_State; + begin + S := Get_First_State (N); + while S /= No_State loop + Set_State_Label (S, Int32 (S)); + S := Get_Next_State (S); + end loop; + end Labelize_States_Debug; + +end PSL.NFAs; diff --git a/src/psl/psl-nfas.ads b/src/psl/psl-nfas.ads new file mode 100644 index 000000000..815acf223 --- /dev/null +++ b/src/psl/psl-nfas.ads @@ -0,0 +1,108 @@ +with Types; use Types; +with PSL.Nodes; use PSL.Nodes; + +package PSL.NFAs is + -- Represents NFAs for PSL. + -- These NFAs have the following restrictions: + -- * 1 start state + -- * 1 final state (which can be the start state). + -- * possible epsilon transition between start and final state with the + -- meaning: A | eps + + type NFA_State is new Nat32; + type NFA_Edge is new Nat32; + + No_NFA : constant NFA := 0; + No_State : constant NFA_State := 0; + No_Edge : constant NFA_Edge := 0; + + -- Create a new NFA. + function Create_NFA return NFA; + + -- Add a new state to an NFA. + function Add_State (N : NFA) return NFA_State; + + -- Add a transition. + procedure Add_Edge (Src : NFA_State; Dest : NFA_State; Expr : Node); + function Add_Edge (Src : NFA_State; Dest : NFA_State; Expr : Node) + return NFA_Edge; + + -- Disconnect and free edge E. + procedure Remove_Edge (E : NFA_Edge); + + -- Return TRUE if there is an epsilon edge between start and final. + function Get_Epsilon_NFA (N : NFA) return Boolean; + procedure Set_Epsilon_NFA (N : NFA; Flag : Boolean); + + -- Each NFA has one start and one final state. + function Get_Start_State (N : NFA) return NFA_State; + procedure Set_Start_State (N : NFA; S : NFA_State); + + procedure Set_Final_State (N : NFA; S : NFA_State); + function Get_Final_State (N : NFA) return NFA_State; + + -- Iterate on all states. + function Get_First_State (N : NFA) return NFA_State; + function Get_Next_State (S : NFA_State) return NFA_State; + + -- Per state user flag. + -- Initialized set to false. + function Get_State_Flag (S : NFA_State) return Boolean; + procedure Set_State_Flag (S : NFA_State; Val : Boolean); + + -- Per state user link. + function Get_State_User_Link (S : NFA_State) return NFA_State; + procedure Set_State_User_Link (S : NFA_State; Link : NFA_State); + + -- Edges of a state. + -- A source edge is an edge whose source is the state. + function Get_First_Src_Edge (N : NFA_State) return NFA_Edge; + function Get_Next_Src_Edge (N : NFA_Edge) return NFA_Edge; + + -- A dest edge is an edge whose destination is the state. + function Get_First_Dest_Edge (N : NFA_State) return NFA_Edge; + function Get_Next_Dest_Edge (N : NFA_Edge) return NFA_Edge; + + function Get_State_Label (S : NFA_State) return Int32; + procedure Set_State_Label (S : NFA_State; Label : Int32); + + function Get_Edge_Dest (E: NFA_Edge) return NFA_State; + function Get_Edge_Src (E : NFA_Edge) return NFA_State; + function Get_Edge_Expr (E : NFA_Edge) return Node; + + -- Move States and edges of R to L. + procedure Merge_NFA (L, R : NFA); + + -- All edges to S are redirected to DEST. + procedure Redest_Edges (S : NFA_State; Dest : NFA_State); + + -- All edges from S are redirected from SRC. + procedure Resource_Edges (S : NFA_State; Src : NFA_State); + + -- Remove a state. The state must be unconnected. + procedure Remove_Unconnected_State (N : NFA; S : NFA_State); + + -- Deconnect and remove state S. + procedure Remove_State (N : NFA; S : NFA_State); + + procedure Delete_Empty_NFA (N : NFA); + + -- Set a label on the states of the NFA N. + -- Start state is has label 0. + -- Return the number of states. + procedure Labelize_States (N : NFA; Nbr_States : out Natural); + + -- Set state index as state label. + -- Used to debug an NFA. + procedure Labelize_States_Debug (N : NFA); + + procedure Set_Edge_Expr (E : NFA_Edge; N : Node); +private + -- Low level procedures. Shouldn't be used directly. + procedure Set_First_Dest_Edge (N : NFA_State; T : NFA_Edge); + procedure Set_Next_Dest_Edge (E : NFA_Edge; N_E : NFA_Edge); + procedure Set_First_Src_Edge (N : NFA_State; T : NFA_Edge); + procedure Set_Next_Src_Edge (E : NFA_Edge; N_E : NFA_Edge); + procedure Set_Edge_Dest (E : NFA_Edge; D : NFA_State); + procedure Set_Edge_Src (E : NFA_Edge; D : NFA_State); +end PSL.NFAs; diff --git a/src/psl/psl-nodes.adb b/src/psl/psl-nodes.adb new file mode 100644 index 000000000..a6482a142 --- /dev/null +++ b/src/psl/psl-nodes.adb @@ -0,0 +1,1231 @@ +-- This is in fact -*- Ada -*- +with Ada.Unchecked_Conversion; +with GNAT.Table; +with PSL.Errors; +with PSL.Hash; + +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, + Format_Medium + ); + + pragma Unreferenced (Format_Type, Format_Short, Format_Medium); + + -- 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 : Int32 + -- Field2 : Int32 + -- Field3 : Int32 + -- Field4 : Int32 + + -- Fields of Format_Short: + -- Field5 : Int32 + -- Field6 : Int32 + + -- Fields of Format_Medium: + -- Odigit1 : Bit3_Type + -- Odigit2 : Bit3_Type + -- State3 : Bit2_Type + -- State4 : Bit2_Type + -- Field5 : Int32 + -- Field6 : Int32 + -- Field7 : Int32 (location) + -- Field8 : Int32 (field1) + -- Field9 : Int32 (field2) + -- Field10 : Int32 (field3) + -- Field11 : Int32 (field4) + -- Field12 : Int32 (field5) + + 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 : Int32; + Field2 : Int32; + Field3 : Int32; + Field4 : Int32; + Field5 : Int32; + Field6 : Int32; + 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 Int32_To_Uns32 is new Ada.Unchecked_Conversion + (Source => Int32, Target => Uns32); + + function Uns32_To_Int32 is new Ada.Unchecked_Conversion + (Source => Uns32, Target => Int32); + + function Int32_To_NFA is new Ada.Unchecked_Conversion + (Source => Int32, Target => NFA); + + function NFA_To_Int32 is new Ada.Unchecked_Conversion + (Source => NFA, Target => Int32); + + 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 : Int32) is + begin + Nodet.Table (N).Field1 := V; + end Set_Field1; + + function Get_Field1 (N : Node) return Int32 is + begin + return Nodet.Table (N).Field1; + end Get_Field1; + + + procedure Set_Field2 (N : Node; V : Int32) is + begin + Nodet.Table (N).Field2 := V; + end Set_Field2; + + function Get_Field2 (N : Node) return Int32 is + begin + return Nodet.Table (N).Field2; + end Get_Field2; + + + function Get_Field3 (N : Node) return Int32 is + begin + return Nodet.Table (N).Field3; + end Get_Field3; + + procedure Set_Field3 (N : Node; V : Int32) is + begin + Nodet.Table (N).Field3 := V; + end Set_Field3; + + + function Get_Field4 (N : Node) return Int32 is + begin + return Nodet.Table (N).Field4; + end Get_Field4; + + procedure Set_Field4 (N : Node; V : Int32) is + begin + Nodet.Table (N).Field4 := V; + end Set_Field4; + + + function Get_Field5 (N : Node) return Int32 is + begin + return Nodet.Table (N).Field5; + end Get_Field5; + + procedure Set_Field5 (N : Node; V : Int32) is + begin + Nodet.Table (N).Field5 := V; + end Set_Field5; + + + function Get_Field6 (N : Node) return Int32 is + begin + return Nodet.Table (N).Field6; + end Get_Field6; + + procedure Set_Field6 (N : Node; V : Int32) is + begin + Nodet.Table (N).Field6 := V; + end Set_Field6; + + procedure Set_Field7 (N : Node; V : Int32) is + begin + Nodet.Table (N + 1).Field1 := V; + end Set_Field7; + + function Get_Field7 (N : Node) return Int32 is + begin + return Nodet.Table (N + 1).Field1; + end Get_Field7; + + + function Create_Node (Kind : Nkind) return Node + is + Res : Node; + begin + if Free_Nodes /= Null_Node then + Res := Free_Nodes; + Free_Nodes := Node (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, Int32 (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); + + pragma Unreferenced (Set_Field7, Get_Field7); + -- Subprograms. + procedure Check_Kind_For_Identifier (N : Node) is + begin + case Get_Kind (N) is + when N_Vmode + | N_Vunit + | N_Vprop + | N_Hdl_Mod_Name + | N_Property_Declaration + | N_Sequence_Declaration + | N_Endpoint_Declaration + | N_Const_Parameter + | N_Boolean_Parameter + | N_Property_Parameter + | N_Sequence_Parameter + | N_Name + | N_Name_Decl => + null; + when others => + Failed ("Get/Set_Identifier", N); + end case; + end Check_Kind_For_Identifier; + + function Get_Identifier (N : Node) return Name_Id is + begin + Check_Kind_For_Identifier (N); + return Name_Id (Get_Field1 (N)); + end Get_Identifier; + + procedure Set_Identifier (N : Node; Id : Name_Id) is + begin + Check_Kind_For_Identifier (N); + Set_Field1 (N, Int32 (Id)); + end Set_Identifier; + + procedure Check_Kind_For_Chain (N : Node) is + begin + case Get_Kind (N) is + when N_Vmode + | N_Vunit + | N_Vprop + | N_Assert_Directive + | N_Property_Declaration + | N_Sequence_Declaration + | N_Endpoint_Declaration + | N_Const_Parameter + | N_Boolean_Parameter + | N_Property_Parameter + | N_Sequence_Parameter + | N_Actual + | N_Name_Decl => + null; + when others => + Failed ("Get/Set_Chain", N); + end case; + end Check_Kind_For_Chain; + + function Get_Chain (N : Node) return Node is + begin + Check_Kind_For_Chain (N); + return Node (Get_Field2 (N)); + end Get_Chain; + + procedure Set_Chain (N : Node; Chain : Node) is + begin + Check_Kind_For_Chain (N); + Set_Field2 (N, Int32 (Chain)); + end Set_Chain; + + procedure Check_Kind_For_Instance (N : Node) is + begin + case Get_Kind (N) is + when N_Vmode + | N_Vunit + | N_Vprop => + null; + when others => + Failed ("Get/Set_Instance", N); + end case; + end Check_Kind_For_Instance; + + function Get_Instance (N : Node) return Node is + begin + Check_Kind_For_Instance (N); + return Node (Get_Field3 (N)); + end Get_Instance; + + procedure Set_Instance (N : Node; Instance : Node) is + begin + Check_Kind_For_Instance (N); + Set_Field3 (N, Int32 (Instance)); + end Set_Instance; + + procedure Check_Kind_For_Item_Chain (N : Node) is + begin + case Get_Kind (N) is + when N_Vmode + | N_Vunit + | N_Vprop => + null; + when others => + Failed ("Get/Set_Item_Chain", N); + end case; + end Check_Kind_For_Item_Chain; + + function Get_Item_Chain (N : Node) return Node is + begin + Check_Kind_For_Item_Chain (N); + return Node (Get_Field4 (N)); + end Get_Item_Chain; + + procedure Set_Item_Chain (N : Node; Item : Node) is + begin + Check_Kind_For_Item_Chain (N); + Set_Field4 (N, Int32 (Item)); + end Set_Item_Chain; + + procedure Check_Kind_For_Prefix (N : Node) is + begin + case Get_Kind (N) is + when N_Hdl_Mod_Name => + null; + when others => + Failed ("Get/Set_Prefix", N); + end case; + end Check_Kind_For_Prefix; + + function Get_Prefix (N : Node) return Node is + begin + Check_Kind_For_Prefix (N); + return Node (Get_Field2 (N)); + end Get_Prefix; + + procedure Set_Prefix (N : Node; Prefix : Node) is + begin + Check_Kind_For_Prefix (N); + Set_Field2 (N, Int32 (Prefix)); + end Set_Prefix; + + procedure Check_Kind_For_Label (N : Node) is + begin + case Get_Kind (N) is + when N_Assert_Directive => + null; + when others => + Failed ("Get/Set_Label", N); + end case; + end Check_Kind_For_Label; + + function Get_Label (N : Node) return Name_Id is + begin + Check_Kind_For_Label (N); + return Name_Id (Get_Field1 (N)); + end Get_Label; + + procedure Set_Label (N : Node; Id : Name_Id) is + begin + Check_Kind_For_Label (N); + Set_Field1 (N, Int32 (Id)); + end Set_Label; + + procedure Check_Kind_For_String (N : Node) is + begin + case Get_Kind (N) is + when N_Assert_Directive => + null; + when others => + Failed ("Get/Set_String", N); + end case; + end Check_Kind_For_String; + + function Get_String (N : Node) return Node is + begin + Check_Kind_For_String (N); + return Node (Get_Field3 (N)); + end Get_String; + + procedure Set_String (N : Node; Str : Node) is + begin + Check_Kind_For_String (N); + Set_Field3 (N, Int32 (Str)); + end Set_String; + + procedure Check_Kind_For_Property (N : Node) is + begin + case Get_Kind (N) is + when N_Assert_Directive + | N_Property_Declaration + | N_Clock_Event + | N_Always + | N_Never + | N_Eventually + | N_Strong + | N_Imp_Seq + | N_Overlap_Imp_Seq + | N_Next + | N_Next_A + | N_Next_E + | N_Next_Event + | N_Next_Event_A + | N_Next_Event_E + | N_Abort => + null; + when others => + Failed ("Get/Set_Property", N); + end case; + end Check_Kind_For_Property; + + function Get_Property (N : Node) return Node is + begin + Check_Kind_For_Property (N); + return Node (Get_Field4 (N)); + end Get_Property; + + procedure Set_Property (N : Node; Property : Node) is + begin + Check_Kind_For_Property (N); + Set_Field4 (N, Int32 (Property)); + end Set_Property; + + procedure Check_Kind_For_NFA (N : Node) is + begin + case Get_Kind (N) is + when N_Assert_Directive => + null; + when others => + Failed ("Get/Set_NFA", N); + end case; + end Check_Kind_For_NFA; + + function Get_NFA (N : Node) return NFA is + begin + Check_Kind_For_NFA (N); + return Int32_To_NFA (Get_Field5 (N)); + end Get_NFA; + + procedure Set_NFA (N : Node; P : NFA) is + begin + Check_Kind_For_NFA (N); + Set_Field5 (N, NFA_To_Int32 (P)); + end Set_NFA; + + procedure Check_Kind_For_Global_Clock (N : Node) is + begin + case Get_Kind (N) is + when N_Property_Declaration => + null; + when others => + Failed ("Get/Set_Global_Clock", N); + end case; + end Check_Kind_For_Global_Clock; + + function Get_Global_Clock (N : Node) return Node is + begin + Check_Kind_For_Global_Clock (N); + return Node (Get_Field3 (N)); + end Get_Global_Clock; + + procedure Set_Global_Clock (N : Node; Clock : Node) is + begin + Check_Kind_For_Global_Clock (N); + Set_Field3 (N, Int32 (Clock)); + end Set_Global_Clock; + + procedure Check_Kind_For_Parameter_List (N : Node) is + begin + case Get_Kind (N) is + when N_Property_Declaration + | N_Sequence_Declaration + | N_Endpoint_Declaration => + null; + when others => + Failed ("Get/Set_Parameter_List", N); + end case; + end Check_Kind_For_Parameter_List; + + function Get_Parameter_List (N : Node) return Node is + begin + Check_Kind_For_Parameter_List (N); + return Node (Get_Field5 (N)); + end Get_Parameter_List; + + procedure Set_Parameter_List (N : Node; E : Node) is + begin + Check_Kind_For_Parameter_List (N); + Set_Field5 (N, Int32 (E)); + end Set_Parameter_List; + + procedure Check_Kind_For_Sequence (N : Node) is + begin + case Get_Kind (N) is + when N_Sequence_Declaration + | N_Endpoint_Declaration + | N_Imp_Seq + | N_Overlap_Imp_Seq + | N_Star_Repeat_Seq + | N_Goto_Repeat_Seq + | N_Plus_Repeat_Seq + | N_Equal_Repeat_Seq => + null; + when others => + Failed ("Get/Set_Sequence", N); + end case; + end Check_Kind_For_Sequence; + + function Get_Sequence (N : Node) return Node is + begin + Check_Kind_For_Sequence (N); + return Node (Get_Field3 (N)); + end Get_Sequence; + + procedure Set_Sequence (N : Node; S : Node) is + begin + Check_Kind_For_Sequence (N); + Set_Field3 (N, Int32 (S)); + end Set_Sequence; + + procedure Check_Kind_For_Actual (N : Node) is + begin + case Get_Kind (N) is + when N_Const_Parameter + | N_Boolean_Parameter + | N_Property_Parameter + | N_Sequence_Parameter + | N_Actual => + null; + when others => + Failed ("Get/Set_Actual", N); + end case; + end Check_Kind_For_Actual; + + function Get_Actual (N : Node) return Node is + begin + Check_Kind_For_Actual (N); + return Node (Get_Field3 (N)); + end Get_Actual; + + procedure Set_Actual (N : Node; E : Node) is + begin + Check_Kind_For_Actual (N); + Set_Field3 (N, Int32 (E)); + end Set_Actual; + + procedure Check_Kind_For_Declaration (N : Node) is + begin + case Get_Kind (N) is + when N_Sequence_Instance + | N_Endpoint_Instance + | N_Property_Instance => + null; + when others => + Failed ("Get/Set_Declaration", N); + end case; + end Check_Kind_For_Declaration; + + function Get_Declaration (N : Node) return Node is + begin + Check_Kind_For_Declaration (N); + return Node (Get_Field1 (N)); + end Get_Declaration; + + procedure Set_Declaration (N : Node; Decl : Node) is + begin + Check_Kind_For_Declaration (N); + Set_Field1 (N, Int32 (Decl)); + end Set_Declaration; + + procedure Check_Kind_For_Association_Chain (N : Node) is + begin + case Get_Kind (N) is + when N_Sequence_Instance + | N_Endpoint_Instance + | N_Property_Instance => + null; + when others => + Failed ("Get/Set_Association_Chain", N); + end case; + end Check_Kind_For_Association_Chain; + + function Get_Association_Chain (N : Node) return Node is + begin + Check_Kind_For_Association_Chain (N); + return Node (Get_Field2 (N)); + end Get_Association_Chain; + + procedure Set_Association_Chain (N : Node; Chain : Node) is + begin + Check_Kind_For_Association_Chain (N); + Set_Field2 (N, Int32 (Chain)); + end Set_Association_Chain; + + procedure Check_Kind_For_Formal (N : Node) is + begin + case Get_Kind (N) is + when N_Actual => + null; + when others => + Failed ("Get/Set_Formal", N); + end case; + end Check_Kind_For_Formal; + + function Get_Formal (N : Node) return Node is + begin + Check_Kind_For_Formal (N); + return Node (Get_Field4 (N)); + end Get_Formal; + + procedure Set_Formal (N : Node; E : Node) is + begin + Check_Kind_For_Formal (N); + Set_Field4 (N, Int32 (E)); + end Set_Formal; + + procedure Check_Kind_For_Boolean (N : Node) is + begin + case Get_Kind (N) is + when N_Clock_Event + | N_Next_Event + | N_Next_Event_A + | N_Next_Event_E + | N_Abort + | N_Not_Bool => + null; + when others => + Failed ("Get/Set_Boolean", N); + end case; + end Check_Kind_For_Boolean; + + function Get_Boolean (N : Node) return Node is + begin + Check_Kind_For_Boolean (N); + return Node (Get_Field3 (N)); + end Get_Boolean; + + procedure Set_Boolean (N : Node; B : Node) is + begin + Check_Kind_For_Boolean (N); + Set_Field3 (N, Int32 (B)); + end Set_Boolean; + + procedure Check_Kind_For_Strong_Flag (N : Node) is + begin + case Get_Kind (N) is + when N_Next + | N_Next_A + | N_Next_E + | N_Next_Event + | N_Next_Event_A + | N_Next_Event_E + | N_Until + | N_Before => + null; + when others => + Failed ("Get/Set_Strong_Flag", N); + end case; + end Check_Kind_For_Strong_Flag; + + function Get_Strong_Flag (N : Node) return Boolean is + begin + Check_Kind_For_Strong_Flag (N); + return Get_Flag1 (N); + end Get_Strong_Flag; + + procedure Set_Strong_Flag (N : Node; B : Boolean) is + begin + Check_Kind_For_Strong_Flag (N); + Set_Flag1 (N, B); + end Set_Strong_Flag; + + procedure Check_Kind_For_Number (N : Node) is + begin + case Get_Kind (N) is + when N_Next + | N_Next_Event => + null; + when others => + Failed ("Get/Set_Number", N); + end case; + end Check_Kind_For_Number; + + function Get_Number (N : Node) return Node is + begin + Check_Kind_For_Number (N); + return Node (Get_Field1 (N)); + end Get_Number; + + procedure Set_Number (N : Node; S : Node) is + begin + Check_Kind_For_Number (N); + Set_Field1 (N, Int32 (S)); + end Set_Number; + + procedure Check_Kind_For_Decl (N : Node) is + begin + case Get_Kind (N) is + when N_Name => + null; + when others => + Failed ("Get/Set_Decl", N); + end case; + end Check_Kind_For_Decl; + + function Get_Decl (N : Node) return Node is + begin + Check_Kind_For_Decl (N); + return Node (Get_Field2 (N)); + end Get_Decl; + + procedure Set_Decl (N : Node; D : Node) is + begin + Check_Kind_For_Decl (N); + Set_Field2 (N, Int32 (D)); + end Set_Decl; + + procedure Check_Kind_For_Value (N : Node) is + begin + case Get_Kind (N) is + when N_Number => + null; + when others => + Failed ("Get/Set_Value", N); + end case; + end Check_Kind_For_Value; + + function Get_Value (N : Node) return Uns32 is + begin + Check_Kind_For_Value (N); + return Int32_To_Uns32 (Get_Field1 (N)); + end Get_Value; + + procedure Set_Value (N : Node; Val : Uns32) is + begin + Check_Kind_For_Value (N); + Set_Field1 (N, Uns32_To_Int32 (Val)); + end Set_Value; + + procedure Check_Kind_For_SERE (N : Node) is + begin + case Get_Kind (N) is + when N_Braced_SERE => + null; + when others => + Failed ("Get/Set_SERE", N); + end case; + end Check_Kind_For_SERE; + + function Get_SERE (N : Node) return Node is + begin + Check_Kind_For_SERE (N); + return Node (Get_Field1 (N)); + end Get_SERE; + + procedure Set_SERE (N : Node; S : Node) is + begin + Check_Kind_For_SERE (N); + Set_Field1 (N, Int32 (S)); + end Set_SERE; + + procedure Check_Kind_For_Left (N : Node) is + begin + case Get_Kind (N) is + when N_Log_Imp_Prop + | N_Until + | N_Before + | N_Or_Prop + | N_And_Prop + | N_Concat_SERE + | N_Fusion_SERE + | N_Within_SERE + | N_Match_And_Seq + | N_And_Seq + | N_Or_Seq + | N_And_Bool + | N_Or_Bool + | N_Imp_Bool => + null; + when others => + Failed ("Get/Set_Left", N); + end case; + end Check_Kind_For_Left; + + function Get_Left (N : Node) return Node is + begin + Check_Kind_For_Left (N); + return Node (Get_Field1 (N)); + end Get_Left; + + procedure Set_Left (N : Node; S : Node) is + begin + Check_Kind_For_Left (N); + Set_Field1 (N, Int32 (S)); + end Set_Left; + + procedure Check_Kind_For_Right (N : Node) is + begin + case Get_Kind (N) is + when N_Log_Imp_Prop + | N_Until + | N_Before + | N_Or_Prop + | N_And_Prop + | N_Concat_SERE + | N_Fusion_SERE + | N_Within_SERE + | N_Match_And_Seq + | N_And_Seq + | N_Or_Seq + | N_And_Bool + | N_Or_Bool + | N_Imp_Bool => + null; + when others => + Failed ("Get/Set_Right", N); + end case; + end Check_Kind_For_Right; + + function Get_Right (N : Node) return Node is + begin + Check_Kind_For_Right (N); + return Node (Get_Field2 (N)); + end Get_Right; + + procedure Set_Right (N : Node; S : Node) is + begin + Check_Kind_For_Right (N); + Set_Field2 (N, Int32 (S)); + end Set_Right; + + procedure Check_Kind_For_Low_Bound (N : Node) is + begin + case Get_Kind (N) is + when N_Next_A + | N_Next_E + | N_Next_Event_A + | N_Next_Event_E + | N_Star_Repeat_Seq + | N_Goto_Repeat_Seq + | N_Equal_Repeat_Seq => + null; + when others => + Failed ("Get/Set_Low_Bound", N); + end case; + end Check_Kind_For_Low_Bound; + + function Get_Low_Bound (N : Node) return Node is + begin + Check_Kind_For_Low_Bound (N); + return Node (Get_Field1 (N)); + end Get_Low_Bound; + + procedure Set_Low_Bound (N : Node; S : Node) is + begin + Check_Kind_For_Low_Bound (N); + Set_Field1 (N, Int32 (S)); + end Set_Low_Bound; + + procedure Check_Kind_For_High_Bound (N : Node) is + begin + case Get_Kind (N) is + when N_Next_A + | N_Next_E + | N_Next_Event_A + | N_Next_Event_E + | N_Star_Repeat_Seq + | N_Goto_Repeat_Seq + | N_Equal_Repeat_Seq => + null; + when others => + Failed ("Get/Set_High_Bound", N); + end case; + end Check_Kind_For_High_Bound; + + function Get_High_Bound (N : Node) return Node is + begin + Check_Kind_For_High_Bound (N); + return Node (Get_Field2 (N)); + end Get_High_Bound; + + procedure Set_High_Bound (N : Node; S : Node) is + begin + Check_Kind_For_High_Bound (N); + Set_Field2 (N, Int32 (S)); + end Set_High_Bound; + + procedure Check_Kind_For_Inclusive_Flag (N : Node) is + begin + case Get_Kind (N) is + when N_Until + | N_Before => + null; + when others => + Failed ("Get/Set_Inclusive_Flag", N); + end case; + end Check_Kind_For_Inclusive_Flag; + + function Get_Inclusive_Flag (N : Node) return Boolean is + begin + Check_Kind_For_Inclusive_Flag (N); + return Get_Flag2 (N); + end Get_Inclusive_Flag; + + procedure Set_Inclusive_Flag (N : Node; B : Boolean) is + begin + Check_Kind_For_Inclusive_Flag (N); + Set_Flag2 (N, B); + end Set_Inclusive_Flag; + + procedure Check_Kind_For_Presence (N : Node) is + begin + case Get_Kind (N) is + when N_Not_Bool + | N_And_Bool + | N_Or_Bool + | N_Imp_Bool + | N_HDL_Expr => + null; + when others => + Failed ("Get/Set_Presence", N); + end case; + end Check_Kind_For_Presence; + + function Get_Presence (N : Node) return PSL_Presence_Kind is + begin + Check_Kind_For_Presence (N); + return PSL_Presence_Kind'Val(Get_State1 (N)); + end Get_Presence; + + procedure Set_Presence (N : Node; P : PSL_Presence_Kind) is + begin + Check_Kind_For_Presence (N); + Set_State1 (N, PSL_Presence_Kind'pos (P)); + end Set_Presence; + + procedure Check_Kind_For_HDL_Node (N : Node) is + begin + case Get_Kind (N) is + when N_HDL_Expr => + null; + when others => + Failed ("Get/Set_HDL_Node", N); + end case; + end Check_Kind_For_HDL_Node; + + function Get_HDL_Node (N : Node) return HDL_Node is + begin + Check_Kind_For_HDL_Node (N); + return Get_Field1 (N); + end Get_HDL_Node; + + procedure Set_HDL_Node (N : Node; H : HDL_Node) is + begin + Check_Kind_For_HDL_Node (N); + Set_Field1 (N, H); + end Set_HDL_Node; + + procedure Check_Kind_For_HDL_Index (N : Node) is + begin + case Get_Kind (N) is + when N_HDL_Expr + | N_EOS => + null; + when others => + Failed ("Get/Set_HDL_Index", N); + end case; + end Check_Kind_For_HDL_Index; + + function Get_HDL_Index (N : Node) return Int32 is + begin + Check_Kind_For_HDL_Index (N); + return Get_Field2 (N); + end Get_HDL_Index; + + procedure Set_HDL_Index (N : Node; Idx : Int32) is + begin + Check_Kind_For_HDL_Index (N); + Set_Field2 (N, Idx); + end Set_HDL_Index; + + procedure Check_Kind_For_Hash (N : Node) is + begin + case Get_Kind (N) is + when N_Not_Bool + | N_And_Bool + | N_Or_Bool + | N_Imp_Bool + | N_HDL_Expr + | N_EOS => + null; + when others => + Failed ("Get/Set_Hash", N); + end case; + end Check_Kind_For_Hash; + + function Get_Hash (N : Node) return Uns32 is + begin + Check_Kind_For_Hash (N); + return Int32_To_Uns32 (Get_Field5 (N)); + end Get_Hash; + + procedure Set_Hash (N : Node; E : Uns32) is + begin + Check_Kind_For_Hash (N); + Set_Field5 (N, Uns32_To_Int32 (E)); + end Set_Hash; + + procedure Check_Kind_For_Hash_Link (N : Node) is + begin + case Get_Kind (N) is + when N_Not_Bool + | N_And_Bool + | N_Or_Bool + | N_Imp_Bool + | N_HDL_Expr + | N_EOS => + null; + when others => + Failed ("Get/Set_Hash_Link", N); + end case; + end Check_Kind_For_Hash_Link; + + function Get_Hash_Link (N : Node) return Node is + begin + Check_Kind_For_Hash_Link (N); + return Node (Get_Field6 (N)); + end Get_Hash_Link; + + procedure Set_Hash_Link (N : Node; E : Node) is + begin + Check_Kind_For_Hash_Link (N); + Set_Field6 (N, Int32 (E)); + end Set_Hash_Link; + + +end PSL.Nodes; + diff --git a/src/psl/psl-nodes.ads b/src/psl/psl-nodes.ads new file mode 100644 index 000000000..241091805 --- /dev/null +++ b/src/psl/psl-nodes.ads @@ -0,0 +1,563 @@ +with Types; use Types; + +package PSL.Nodes is + type Nkind is + ( + N_Error, + + N_Vmode, + N_Vunit, + N_Vprop, + + N_Hdl_Mod_Name, + + N_Assert_Directive, + N_Property_Declaration, + N_Sequence_Declaration, + N_Endpoint_Declaration, + + -- Formal parameters + N_Const_Parameter, + N_Boolean_Parameter, + N_Property_Parameter, + N_Sequence_Parameter, + + N_Sequence_Instance, + N_Endpoint_Instance, + N_Property_Instance, + N_Actual, + + N_Clock_Event, + + -- Properties + N_Always, + N_Never, + N_Eventually, + N_Strong, -- ! + N_Imp_Seq, -- |=> + N_Overlap_Imp_Seq, -- |-> + N_Log_Imp_Prop, -- -> + N_Next, + N_Next_A, + N_Next_E, + N_Next_Event, + N_Next_Event_A, + N_Next_Event_E, + N_Abort, + N_Until, + N_Before, + N_Or_Prop, + N_And_Prop, + + -- Sequences/SERE. + N_Braced_SERE, + N_Concat_SERE, + N_Fusion_SERE, + N_Within_SERE, + + N_Match_And_Seq, -- && + N_And_Seq, + N_Or_Seq, + + N_Star_Repeat_Seq, + N_Goto_Repeat_Seq, + N_Plus_Repeat_Seq, -- [+] + N_Equal_Repeat_Seq, + + -- Boolean layer. + N_Not_Bool, + N_And_Bool, + N_Or_Bool, + N_Imp_Bool, -- -> + N_HDL_Expr, + N_False, + N_True, + N_EOS, + + N_Name, + N_Name_Decl, + N_Number + ); + for Nkind'Size use 8; + + subtype N_Booleans is Nkind range N_Not_Bool .. N_True; + subtype N_Sequences is Nkind range N_Braced_SERE .. N_Equal_Repeat_Seq; + + type PSL_Types is + ( + Type_Unknown, + Type_Boolean, + Type_Bit, + Type_Bitvector, + Type_Numeric, + Type_String, + Type_Sequence, + Type_Property + ); + + -- Within CSE, it is useful to know which sub-expression already compose + -- an expression. + -- Eg: suppose we want to build A and B. + -- Each sub-expressions of B is marked either as Present_Pos or + -- Present_Neg. + -- If A is already present, return either B or FALSE. + -- Otherwise, build the node. + type PSL_Presence_Kind is + ( + Present_Unknown, + Present_Pos, + Present_Neg + ); + + -- Start of nodes: + + -- N_Error (Short) + + -- N_Vmode (Short) + -- N_Vunit (Short) + -- N_Vprop (Short) + -- + -- Get/Set_Identifier (Field1) + -- + -- Get/Set_Chain (Field2) + -- + -- Get/Set_Instance (Field3) + -- + -- Get/Set_Item_Chain (Field4) + + -- N_Hdl_Mod_Name (Short) + -- + -- Get/Set_Identifier (Field1) + -- + -- Get/Set_Prefix (Field2) + + -- N_Assert_Directive (Short) + -- + -- Get/Set_Label (Field1) + -- + -- Get/Set_Chain (Field2) + -- + -- Get/Set_String (Field3) + -- + -- Get/Set_Property (Field4) + -- + -- Get/Set_NFA (Field5) + + -- N_Property_Declaration (Short) + -- + -- Get/Set_Identifier (Field1) + -- + -- Get/Set_Chain (Field2) + -- + -- Get/Set_Global_Clock (Field3) + -- + -- Get/Set_Property (Field4) + -- + -- Get/Set_Parameter_List (Field5) + + -- N_Sequence_Declaration (Short) + -- N_Endpoint_Declaration (Short) + -- + -- Get/Set_Identifier (Field1) + -- + -- Get/Set_Chain (Field2) + -- + -- Get/Set_Sequence (Field3) + -- + -- Get/Set_Parameter_List (Field5) + + -- N_Const_Parameter (Short) + -- N_Boolean_Parameter (Short) + -- N_Property_Parameter (Short) + -- N_Sequence_Parameter (Short) + -- + -- Get/Set_Identifier (Field1) + -- + -- Get/Set_Chain (Field2) + -- + -- -- Current actual parameter. + -- Get/Set_Actual (Field3) + + -- N_Sequence_Instance (Short) + -- N_Endpoint_Instance (Short) + -- N_Property_Instance (Short) + -- + -- Get/Set_Declaration (Field1) [Flat] + -- + -- Get/Set_Association_Chain (Field2) + + -- N_Actual (Short) + -- + -- Get/Set_Chain (Field2) + -- + -- Get/Set_Actual (Field3) + -- + -- Get/Set_Formal (Field4) + + -- N_Clock_Event (Short) + -- + -- Get/Set_Property (Field4) + -- + -- Get/Set_Boolean (Field3) + + -- N_Always (Short) + -- N_Never (Short) + -- N_Eventually (Short) + -- N_Strong (Short) + -- + -- Get/Set_Property (Field4) + + -- N_Next (Short) + -- + -- Get/Set_Strong_Flag (Flag1) + -- + -- Get/Set_Number (Field1) + -- + -- Get/Set_Property (Field4) + + -- N_Name (Short) + -- + -- Get/Set_Identifier (Field1) + -- + -- Get/Set_Decl (Field2) + + -- N_Name_Decl (Short) + -- + -- Get/Set_Identifier (Field1) + -- + -- Get/Set_Chain (Field2) + + -- N_Number (Short) + -- + -- Get/Set_Value (Field1) + + -- N_Braced_SERE (Short) + -- + -- Get/Set_SERE (Field1) + + -- N_Concat_SERE (Short) + -- N_Fusion_SERE (Short) + -- N_Within_SERE (Short) + -- + -- Get/Set_Left (Field1) + -- + -- Get/Set_Right (Field2) + + -- N_Star_Repeat_Seq (Short) + -- N_Goto_Repeat_Seq (Short) + -- N_Equal_Repeat_Seq (Short) + -- + -- Note: can be null_node for star_repeat_seq. + -- Get/Set_Sequence (Field3) + -- + -- Get/Set_Low_Bound (Field1) + -- + -- Get/Set_High_Bound (Field2) + + -- N_Plus_Repeat_Seq (Short) + -- + -- Note: can be null_node. + -- Get/Set_Sequence (Field3) + + -- N_Match_And_Seq (Short) + -- N_And_Seq (Short) + -- N_Or_Seq (Short) + -- + -- Get/Set_Left (Field1) + -- + -- Get/Set_Right (Field2) + + -- N_Imp_Seq (Short) + -- N_Overlap_Imp_Seq (Short) + -- + -- Get/Set_Sequence (Field3) + -- + -- Get/Set_Property (Field4) + + -- N_Log_Imp_Prop (Short) + -- + -- Get/Set_Left (Field1) + -- + -- Get/Set_Right (Field2) + + -- N_Next_A (Short) + -- N_Next_E (Short) + -- + -- Get/Set_Strong_Flag (Flag1) + -- + -- Get/Set_Low_Bound (Field1) + -- + -- Get/Set_High_Bound (Field2) + -- + -- Get/Set_Property (Field4) + + -- N_Next_Event (Short) + -- + -- Get/Set_Strong_Flag (Flag1) + -- + -- Get/Set_Number (Field1) + -- + -- Get/Set_Property (Field4) + -- + -- Get/Set_Boolean (Field3) + + -- N_Or_Prop (Short) + -- N_And_Prop (Short) + -- + -- Get/Set_Left (Field1) + -- + -- Get/Set_Right (Field2) + + -- N_Until (Short) + -- N_Before (Short) + -- + -- Get/Set_Strong_Flag (Flag1) + -- + -- Get/Set_Inclusive_Flag (Flag2) + -- + -- Get/Set_Left (Field1) + -- + -- Get/Set_Right (Field2) + + -- N_Next_Event_A (Short) + -- N_Next_Event_E (Short) + -- + -- Get/Set_Strong_Flag (Flag1) + -- + -- Get/Set_Low_Bound (Field1) + -- + -- Get/Set_High_Bound (Field2) + -- + -- Get/Set_Property (Field4) + -- + -- Get/Set_Boolean (Field3) + + -- N_Abort (Short) + -- + -- Get/Set_Property (Field4) + -- + -- Get/Set_Boolean (Field3) + + + -- N_HDL_Expr (Short) + -- + -- Get/Set_Presence (State1) + -- + -- Get/Set_HDL_Node (Field1) + -- + -- Get/Set_HDL_Index (Field2) + -- + -- Get/Set_Hash (Field5) + -- + -- Get/Set_Hash_Link (Field6) + + -- N_Not_Bool (Short) + -- + -- Get/Set_Presence (State1) + -- + -- Get/Set_Boolean (Field3) + -- + -- Get/Set_Hash (Field5) + -- + -- Get/Set_Hash_Link (Field6) + + -- N_And_Bool (Short) + -- N_Or_Bool (Short) + -- N_Imp_Bool (Short) + -- + -- Get/Set_Presence (State1) + -- + -- Get/Set_Left (Field1) + -- + -- Get/Set_Right (Field2) + -- + -- Get/Set_Hash (Field5) + -- + -- Get/Set_Hash_Link (Field6) + + -- N_True (Short) + -- N_False (Short) + + -- N_EOS (Short) + -- End of simulation. + -- + -- Get/Set_HDL_Index (Field2) + -- + -- Get/Set_Hash (Field5) + -- + -- Get/Set_Hash_Link (Field6) + + -- End of nodes. + + subtype Node is Types.PSL_Node; + + Null_Node : constant Node := 0; + False_Node : constant Node := 1; + True_Node : constant Node := 2; + One_Node : constant Node := 3; + EOS_Node : constant Node := 4; + + subtype NFA is Types.PSL_NFA; + + subtype HDL_Node is Types.Int32; + HDL_Null : constant HDL_Node := 0; + + procedure Init; + + -- Get the number of the last node. + -- To be used to size lateral tables. + function Get_Last_Node return Node; + + -- subtype Regs_Type_Node is Node range Reg_Type_Node .. Time_Type_Node; + + function Create_Node (Kind : Nkind) return Node; + procedure Free_Node (N : Node); + + -- Return the type of a node. + function Get_Psl_Type (N : Node) return PSL_Types; + + -- Field: Location + function Get_Location (N : Node) return Location_Type; + procedure Set_Location (N : Node; Loc : Location_Type); + + function Get_Kind (N : Node) return Nkind; + pragma Inline (Get_Kind); + +-- -- Disp: None +-- -- Field: Field6 +-- function Get_Parent (N : Node) return Node; +-- procedure Set_Parent (N : Node; Parent : Node); + + -- Disp: Special + -- Field: Field1 (conv) + function Get_Identifier (N : Node) return Name_Id; + procedure Set_Identifier (N : Node; Id : Name_Id); + + -- Disp: Special + -- Field: Field1 (conv) + function Get_Label (N : Node) return Name_Id; + procedure Set_Label (N : Node; Id : Name_Id); + + -- Disp: Chain + -- Field: Field2 (conv) + function Get_Chain (N : Node) return Node; + procedure Set_Chain (N : Node; Chain : Node); + + -- Field: Field3 (conv) + function Get_Instance (N : Node) return Node; + procedure Set_Instance (N : Node; Instance : Node); + + -- Field: Field2 (conv) + function Get_Prefix (N : Node) return Node; + procedure Set_Prefix (N : Node; Prefix : Node); + + -- Field: Field4 (conv) + function Get_Item_Chain (N : Node) return Node; + procedure Set_Item_Chain (N : Node; Item : Node); + + -- Field: Field4 (conv) + function Get_Property (N : Node) return Node; + procedure Set_Property (N : Node; Property : Node); + + -- Field: Field3 (conv) + function Get_String (N : Node) return Node; + procedure Set_String (N : Node; Str : Node); + + -- Field: Field1 (conv) + function Get_SERE (N : Node) return Node; + procedure Set_SERE (N : Node; S : Node); + + -- Field: Field1 (conv) + function Get_Left (N : Node) return Node; + procedure Set_Left (N : Node; S : Node); + + -- Field: Field2 (conv) + function Get_Right (N : Node) return Node; + procedure Set_Right (N : Node; S : Node); + + -- Field: Field3 (conv) + function Get_Sequence (N : Node) return Node; + procedure Set_Sequence (N : Node; S : Node); + + -- Field: Flag1 + function Get_Strong_Flag (N : Node) return Boolean; + procedure Set_Strong_Flag (N : Node; B : Boolean); + + -- Field: Flag2 + function Get_Inclusive_Flag (N : Node) return Boolean; + procedure Set_Inclusive_Flag (N : Node; B : Boolean); + + -- Field: Field1 (conv) + function Get_Low_Bound (N : Node) return Node; + procedure Set_Low_Bound (N : Node; S : Node); + + -- Field: Field2 (conv) + function Get_High_Bound (N : Node) return Node; + procedure Set_High_Bound (N : Node; S : Node); + + -- Field: Field1 (conv) + function Get_Number (N : Node) return Node; + procedure Set_Number (N : Node; S : Node); + + -- Field: Field1 (uc) + function Get_Value (N : Node) return Uns32; + procedure Set_Value (N : Node; Val : Uns32); + + -- Field: Field3 (conv) + function Get_Boolean (N : Node) return Node; + procedure Set_Boolean (N : Node; B : Node); + + -- Field: Field2 (conv) + function Get_Decl (N : Node) return Node; + procedure Set_Decl (N : Node; D : Node); + + -- Field: Field1 (conv) + function Get_HDL_Node (N : Node) return HDL_Node; + procedure Set_HDL_Node (N : Node; H : HDL_Node); + + -- Field: Field5 (uc) + function Get_Hash (N : Node) return Uns32; + procedure Set_Hash (N : Node; E : Uns32); + pragma Inline (Get_Hash); + + -- Field: Field6 (conv) + function Get_Hash_Link (N : Node) return Node; + procedure Set_Hash_Link (N : Node; E : Node); + pragma Inline (Get_Hash_Link); + + -- Field: Field2 + function Get_HDL_Index (N : Node) return Int32; + procedure Set_HDL_Index (N : Node; Idx : Int32); + + -- Field: State1 (pos) + function Get_Presence (N : Node) return PSL_Presence_Kind; + procedure Set_Presence (N : Node; P : PSL_Presence_Kind); + + -- Field: Field5 (uc) + function Get_NFA (N : Node) return NFA; + procedure Set_NFA (N : Node; P : NFA); + + -- Field: Field5 (conv) + function Get_Parameter_List (N : Node) return Node; + procedure Set_Parameter_List (N : Node; E : Node); + + -- Field: Field3 (conv) + function Get_Actual (N : Node) return Node; + procedure Set_Actual (N : Node; E : Node); + + -- Field: Field4 (conv) + function Get_Formal (N : Node) return Node; + procedure Set_Formal (N : Node; E : Node); + + -- Field: Field1 (conv) + function Get_Declaration (N : Node) return Node; + procedure Set_Declaration (N : Node; Decl : Node); + + -- Field: Field2 (conv) + function Get_Association_Chain (N : Node) return Node; + procedure Set_Association_Chain (N : Node; Chain : Node); + + -- Field: Field3 (conv) + function Get_Global_Clock (N : Node) return Node; + procedure Set_Global_Clock (N : Node; Clock : Node); +end PSL.Nodes; diff --git a/src/psl/psl-optimize.adb b/src/psl/psl-optimize.adb new file mode 100644 index 000000000..4ca62b89e --- /dev/null +++ b/src/psl/psl-optimize.adb @@ -0,0 +1,460 @@ +with Types; use Types; +with PSL.NFAs.Utils; use PSL.NFAs.Utils; +with PSL.CSE; + +package body PSL.Optimize is + procedure Push (Head : in out NFA_State; S : NFA_State) is + begin + Set_State_User_Link (S, Head); + Head := S; + end Push; + + procedure Pop (Head : in out NFA_State; S : out NFA_State) is + begin + S := Head; + Head := Get_State_User_Link (S); + end Pop; + + procedure Remove_Unreachable_States (N : NFA) + is + Head : NFA_State; + Start, Final : NFA_State; + E : NFA_Edge; + S, N_S : NFA_State; + begin + -- Remove unreachable states, ie states that can't be reached from + -- start state. + Start := Get_Start_State (N); + Final := Get_Final_State (N); + + Head := No_State; + + -- The start state is reachable. + Push (Head, Start); + Set_State_Flag (Start, True); + + -- Follow edges and mark reachable states. + while Head /= No_State loop + Pop (Head, S); + E := Get_First_Src_Edge (S); + while E /= No_Edge loop + S := Get_Edge_Dest (E); + if not Get_State_Flag (S) then + Push (Head, S); + Set_State_Flag (S, True); + end if; + E := Get_Next_Src_Edge (E); + end loop; + end loop; + + -- Remove unreachable states. + S := Get_First_State (N); + while S /= No_State loop + N_S := Get_Next_State (S); + if Get_State_Flag (S) then + -- Clean-up. + Set_State_Flag (S, False); + elsif S = Final then + -- Do not remove final state! + -- FIXME: deconnect state? + null; + else + Remove_State (N, S); + end if; + S := N_S; + end loop; + + -- Remove no-where states, ie states that can't reach the final state. + Head := No_State; + + -- The final state can reach the final state. + Push (Head, Final); + Set_State_Flag (Final, True); + + -- Follow edges and mark reachable states. + while Head /= No_State loop + Pop (Head, S); + E := Get_First_Dest_Edge (S); + while E /= No_Edge loop + S := Get_Edge_Src (E); + if not Get_State_Flag (S) then + Push (Head, S); + Set_State_Flag (S, True); + end if; + E := Get_Next_Dest_Edge (E); + end loop; + end loop; + + -- Remove unreachable states. + S := Get_First_State (N); + while S /= No_State loop + N_S := Get_Next_State (S); + if Get_State_Flag (S) then + -- Clean-up. + Set_State_Flag (S, False); + elsif S = Start then + -- Do not remove start state! + -- FIXME: deconnect state? + null; + else + Remove_State (N, S); + end if; + S := N_S; + end loop; + end Remove_Unreachable_States; + + procedure Remove_Simple_Prefix (N : NFA) + is + Start : NFA_State; + D : NFA_State; + T_Start, T_D, Next_T_D : NFA_Edge; + T_Expr : Node; + Clean : Boolean := False; + begin + Start := Get_Start_State (N); + + -- Iterate on edges from the start state. + T_Start := Get_First_Src_Edge (Start); + while T_Start /= No_Edge loop + -- Edge destination. + D := Get_Edge_Dest (T_Start); + T_Expr := Get_Edge_Expr (T_Start); + + -- Iterate on destination incoming edges. + T_D := Get_First_Dest_Edge (D); + while T_D /= No_Edge loop + Next_T_D := Get_Next_Dest_Edge (T_D); + -- Remove parallel edge. + if T_D /= T_Start + and then Get_Edge_Expr (T_D) = T_Expr + then + Remove_Edge (T_D); + Clean := True; + end if; + T_D := Next_T_D; + end loop; + T_Start := Get_Next_Src_Edge (T_Start); + end loop; + if Clean then + Remove_Unreachable_States (N); + end if; + end Remove_Simple_Prefix; + + -- Return TRUE iff the outgoing or incoming edges of L and R are the same. + -- Outgoing edges must be sorted. + generic + with function Get_First_Edge (S : NFA_State) return NFA_Edge; + with function Get_Next_Edge (E : NFA_Edge) return NFA_Edge; + with function Get_Edge_State_Reverse (E : NFA_Edge) return NFA_State; + function Are_States_Identical_Gen (L, R : NFA_State) return Boolean; + + function Are_States_Identical_Gen (L, R : NFA_State) return Boolean + is + L_E, R_E : NFA_Edge; + L_S, R_S : NFA_State; + begin + L_E := Get_First_Edge (L); + R_E := Get_First_Edge (R); + loop + if L_E = No_Edge and then R_E = No_Edge then + -- End of chain for both L and R -> identical states. + return True; + elsif L_E = No_Edge or R_E = No_Edge then + -- End of chain for either L or R -> non identical states. + return False; + elsif Get_Edge_Expr (L_E) /= Get_Edge_Expr (R_E) then + -- Different edge (different expressions). + return False; + end if; + L_S := Get_Edge_State_Reverse (L_E); + R_S := Get_Edge_State_Reverse (R_E); + if L_S /= R_S and then (L_S /= L or else R_S /= R) then + -- Predecessors are differents and not loop. + return False; + end if; + L_E := Get_Next_Edge (L_E); + R_E := Get_Next_Edge (R_E); + end loop; + end Are_States_Identical_Gen; + + generic + with procedure Sort_Edges (N : NFA); + with procedure Sort_Edges_Reverse (S : NFA_State); + with function Get_First_Edge (S : NFA_State) return NFA_Edge; + with function Get_Next_Edge (E : NFA_Edge) return NFA_Edge; + with function Get_First_Edge_Reverse (S : NFA_State) return NFA_Edge; + with function Get_Next_Edge_Reverse (E : NFA_Edge) return NFA_Edge; + with function Get_Edge_State (E : NFA_Edge) return NFA_State; + with function Get_Edge_State_Reverse (E : NFA_Edge) return NFA_State; + with procedure Merge_State_Reverse (N : NFA; + S : NFA_State; S1 : NFA_State); + procedure Merge_Identical_States_Gen (N : NFA); + + procedure Merge_Identical_States_Gen (N : NFA) + is + function Are_States_Identical is new Are_States_Identical_Gen + (Get_First_Edge => Get_First_Edge, + Get_Next_Edge => Get_Next_Edge, + Get_Edge_State_Reverse => Get_Edge_State_Reverse); + + S : NFA_State; + E : NFA_Edge; + E_State, Next_E_State : NFA_State; + Next_E, Next_Next_E : NFA_Edge; + begin + Sort_Edges (N); + + -- Iterate on states. + S := Get_First_State (N); + while S /= No_State loop + Sort_Edges_Reverse (S); + + -- Iterate on incoming edges. + E := Get_First_Edge_Reverse (S); + while E /= No_Edge loop + E_State := Get_Edge_State (E); + + -- Try to merge E with its successors. + Next_E := Get_Next_Edge_Reverse (E); + while Next_E /= No_Edge + and then Get_Edge_Expr (E) = Get_Edge_Expr (Next_E) + loop + Next_E_State := Get_Edge_State (Next_E); + Next_Next_E := Get_Next_Edge_Reverse (Next_E); + if Next_E_State = E_State then + -- Identical edge: remove the duplicate. + Remove_Edge (Next_E); + elsif Are_States_Identical (E_State, Next_E_State) then + Merge_State_Reverse (N, E_State, Next_E_State); + end if; + Next_E := Next_Next_E; + end loop; + + E := Get_Next_Edge_Reverse (E); + end loop; + + S := Get_Next_State (S); + end loop; + end Merge_Identical_States_Gen; + + procedure Merge_Identical_States_Src is new Merge_Identical_States_Gen + (Sort_Edges => Sort_Src_Edges, + Sort_Edges_Reverse => Sort_Dest_Edges, + Get_First_Edge => Get_First_Src_Edge, + Get_Next_Edge => Get_Next_Src_Edge, + Get_First_Edge_Reverse => Get_First_Dest_Edge, + Get_Next_Edge_Reverse => Get_Next_Dest_Edge, + Get_Edge_State => Get_Edge_Src, + Get_Edge_State_Reverse => Get_Edge_Dest, + Merge_State_Reverse => Merge_State_Dest); + + procedure Merge_Identical_States_Dest is new Merge_Identical_States_Gen + (Sort_Edges => Sort_Dest_Edges, + Sort_Edges_Reverse => Sort_Src_Edges, + Get_First_Edge => Get_First_Dest_Edge, + Get_Next_Edge => Get_Next_Dest_Edge, + Get_First_Edge_Reverse => Get_First_Src_Edge, + Get_Next_Edge_Reverse => Get_Next_Src_Edge, + Get_Edge_State => Get_Edge_Dest, + Get_Edge_State_Reverse => Get_Edge_Src, + Merge_State_Reverse => Merge_State_Src); + + procedure Merge_Identical_States (N : NFA) is + begin + Merge_Identical_States_Src (N); + Merge_Identical_States_Dest (N); + end Merge_Identical_States; + + procedure Merge_Edges (N : NFA) + is + use PSL.CSE; + Nbr_States : Natural; + begin + Labelize_States (N, Nbr_States); + declare + Last_State : constant Int32 := Int32 (Nbr_States) - 1; + type Edge_Array is array (0 .. Last_State) of NFA_Edge; + Edges : Edge_Array; + S, D : NFA_State; + L_D : Int32; + E, Next_E : NFA_Edge; + begin + -- Iterate on states. + S := Get_First_State (N); + while S /= No_State loop + + Edges := (others => No_Edge); + E := Get_First_Src_Edge (S); + while E /= No_Edge loop + Next_E := Get_Next_Src_Edge (E); + D := Get_Edge_Dest (E); + L_D := Get_State_Label (D); + if Edges (L_D) /= No_Edge then + Set_Edge_Expr + (Edges (L_D), + Build_Bool_Or (Get_Edge_Expr (Edges (L_D)), + Get_Edge_Expr (E))); + -- FIXME: reduce expression. + Remove_Edge (E); + else + Edges (L_D) := E; + end if; + E := Next_E; + end loop; + + S := Get_Next_State (S); + end loop; + end; + end Merge_Edges; + + procedure Remove_Identical_Src_Edges (S : NFA_State) + is + Next_E, E : NFA_Edge; + begin + Sort_Src_Edges (S); + E := Get_First_Src_Edge (S); + if E = No_Edge then + return; + end if; + loop + Next_E := Get_Next_Src_Edge (E); + exit when Next_E = No_Edge; + if Get_Edge_Dest (E) = Get_Edge_Dest (Next_E) + and then Get_Edge_Expr (E) = Get_Edge_Expr (Next_E) + then + Remove_Edge (Next_E); + else + E := Next_E; + end if; + end loop; + end Remove_Identical_Src_Edges; + + procedure Remove_Identical_Dest_Edges (S : NFA_State) + is + Next_E, E : NFA_Edge; + begin + Sort_Dest_Edges (S); + E := Get_First_Dest_Edge (S); + if E = No_Edge then + return; + end if; + loop + Next_E := Get_Next_Dest_Edge (E); + exit when Next_E = No_Edge; + if Get_Edge_Src (E) = Get_Edge_Src (Next_E) + and then Get_Edge_Expr (E) = Get_Edge_Expr (Next_E) + then + Remove_Edge (Next_E); + else + E := Next_E; + end if; + end loop; + end Remove_Identical_Dest_Edges; + + procedure Find_Partitions (N : NFA; Nbr_States : Natural) + is + Last_State : constant NFA_State := NFA_State (Nbr_States) - 1; + type Part_Offset is new Int32 range -1 .. Nat32 (Nbr_States - 1); + type Part_Id is new Part_Offset range 0 .. Part_Offset'Last; + + -- State to partition id. + State_Part : array (0 .. Last_State) of Part_Id; + pragma Unreferenced (State_Part); + + -- Last partition index. + Last_Part : Part_Id; + + -- Partitions content. + + -- To get the states in a partition P, first get the offset OFF + -- (from Offsets) of P. States are in Parts (OFF ...). The + -- number of states is not known, but they all belong to P + -- (check with STATE_PART). + Parts : array (Part_Offset) of NFA_State; + type Offset_Array is array (Part_Id) of Part_Offset; + Start_Offsets : Offset_Array; + Last_Offsets : Offset_Array; + + S, Final_State : NFA_State; + First_S : NFA_State; + Off, Last_Off : Part_Offset; + + Stable, Stable1 : Boolean; + + function Is_Equivalent (L, R : NFA_State) return Boolean is + begin + raise Program_Error; + return False; + end Is_Equivalent; + begin + -- Return now for trivial cases (0 or 1 state). + if Nbr_States < 2 then + return; + end if; + + -- Partition 1 contains the final state. + -- Partition 0 contains the other states. + Final_State := Get_Final_State (N); + Last_Part := 1; + State_Part := (others => 0); + State_Part (Final_State) := 1; + S := Get_First_State (N); + Off := -1; + while S /= No_State loop + if S /= Last_State then + Off := Off + 1; + Parts (Off) := S; + end if; + S := Get_Next_State (S); + end loop; + Start_Offsets (0) := 0; + Last_Offsets (0) := Off; + Start_Offsets (1) := Off + 1; + Last_Offsets (1) := Off + 1; + Parts (Off + 1) := Final_State; + + -- Now the hard work. + loop + Stable := True; + -- For every partition + for P in 0 .. Last_Part loop + Off := Start_Offsets (P); + First_S := Parts (Off); + Off := Off + 1; + + -- For every S != First_S in P. + Last_Off := Last_Offsets (P); + Stable1 := True; + while Off <= Last_Off loop + S := Parts (Off); + + if not Is_Equivalent (First_S, S) then + -- Swap S with the last element of the partition. + Parts (Off) := Parts (Last_Off); + Parts (Last_Off) := S; + -- Reduce partition size. + Last_Off := Last_Off - 1; + Last_Offsets (P) := Last_Off; + + if Stable1 then + -- Create a new partition. + Last_Part := Last_Part + 1; + Last_Offsets (Last_Part) := Last_Off + 1; + Stable1 := False; + end if; + -- Put S in the new partition. + Start_Offsets (Last_Part) := Last_Off + 1; + State_Part (S) := Last_Part; + Stable := False; + + -- And continue with the swapped state. + else + Off := Off + 1; + end if; + end loop; + end loop; + exit when Stable; + end loop; + end Find_Partitions; + pragma Unreferenced (Find_Partitions); +end PSL.Optimize; diff --git a/src/psl/psl-optimize.ads b/src/psl/psl-optimize.ads new file mode 100644 index 000000000..5f36a0739 --- /dev/null +++ b/src/psl/psl-optimize.ads @@ -0,0 +1,24 @@ +with PSL.NFAs; use PSL.NFAs; +with PSL.Nodes; use PSL.Nodes; + +package PSL.Optimize is + -- Remove unreachable states, ie + -- * states that can't be reach from the start state. + -- * states that can't reach the final state. + -- O(N) algorithm. + procedure Remove_Unreachable_States (N : NFA); + + -- Remove single prefix, ie edges to a state S that is also from start + -- to S. + -- O(M) algorithm. + procedure Remove_Simple_Prefix (N : NFA); + + procedure Merge_Identical_States (N : NFA); + + procedure Merge_Edges (N : NFA); + + procedure Remove_Identical_Src_Edges (S : NFA_State); + procedure Remove_Identical_Dest_Edges (S : NFA_State); + + --procedure Find_Partitions (N : NFA; Nbr_States : Natural); +end PSL.Optimize; diff --git a/src/psl/psl-prints.adb b/src/psl/psl-prints.adb new file mode 100644 index 000000000..80da47dab --- /dev/null +++ b/src/psl/psl-prints.adb @@ -0,0 +1,433 @@ +with Types; use Types; +with PSL.Errors; use PSL.Errors; +with Name_Table; use Name_Table; +with Ada.Text_IO; use Ada.Text_IO; + +package body PSL.Prints is + function Get_Priority (N : Node) return Priority is + begin + case Get_Kind (N) is + when N_Never | N_Always => + return Prio_FL_Invariance; + when N_Eventually + | N_Next + | N_Next_A + | N_Next_E + | N_Next_Event + | N_Next_Event_A + | N_Next_Event_E => + return Prio_FL_Occurence; + when N_Braced_SERE => + return Prio_SERE_Brace; + when N_Concat_SERE => + return Prio_Seq_Concat; + when N_Fusion_SERE => + return Prio_Seq_Fusion; + when N_Within_SERE => + return Prio_Seq_Within; + when N_Match_And_Seq + | N_And_Seq => + return Prio_Seq_And; + when N_Or_Seq => + return Prio_Seq_Or; + when N_Until + | N_Before => + return Prio_FL_Bounding; + when N_Abort => + return Prio_FL_Abort; + when N_Or_Prop => + return Prio_Seq_Or; + when N_And_Prop => + return Prio_Seq_And; + when N_Imp_Seq + | N_Overlap_Imp_Seq + | N_Log_Imp_Prop + | N_Imp_Bool => + return Prio_Bool_Imp; + when N_Name_Decl + | N_Number + | N_True + | N_False + | N_EOS + | N_HDL_Expr => + return Prio_HDL; + when N_Or_Bool => + return Prio_Seq_Or; + when N_And_Bool => + return Prio_Seq_And; + when N_Not_Bool => + return Prio_Bool_Not; + when N_Star_Repeat_Seq + | N_Goto_Repeat_Seq + | N_Equal_Repeat_Seq + | N_Plus_Repeat_Seq => + return Prio_SERE_Repeat; + when N_Strong => + return Prio_Strong; + when others => + Error_Kind ("get_priority", N); + end case; + end Get_Priority; + + procedure Print_HDL_Expr (N : HDL_Node) is + begin + Put (Image (Get_Identifier (Node (N)))); + end Print_HDL_Expr; + + procedure Dump_Expr (N : Node) + is + begin + case Get_Kind (N) is + when N_HDL_Expr => + if HDL_Expr_Printer = null then + Put ("Expr"); + else + HDL_Expr_Printer.all (Get_HDL_Node (N)); + end if; + when N_True => + Put ("TRUE"); + when N_False => + Put ("FALSE"); + when N_Not_Bool => + Put ("!"); + Dump_Expr (Get_Boolean (N)); + when N_And_Bool => + Put ("("); + Dump_Expr (Get_Left (N)); + Put (" && "); + Dump_Expr (Get_Right (N)); + Put (")"); + when N_Or_Bool => + Put ("("); + Dump_Expr (Get_Left (N)); + Put (" || "); + Dump_Expr (Get_Right (N)); + Put (")"); + when others => + PSL.Errors.Error_Kind ("dump_expr", N); + end case; + end Dump_Expr; + + procedure Print_Expr (N : Node; Parent_Prio : Priority := Prio_Lowest) + is + Prio : Priority; + begin + if N = Null_Node then + Put ("."); + return; + end if; + Prio := Get_Priority (N); + if Prio < Parent_Prio then + Put ("("); + end if; + case Get_Kind (N) is + when N_Number => + declare + Str : constant String := Uns32'Image (Get_Value (N)); + begin + Put (Str (2 .. Str'Last)); + end; + when N_Name_Decl => + Put (Image (Get_Identifier (N))); + when N_HDL_Expr => + if HDL_Expr_Printer = null then + Put ("HDL_Expr"); + else + HDL_Expr_Printer.all (Get_HDL_Node (N)); + end if; + -- FIXME: this is true only when using the scanner. + -- Print_Expr (Node (Get_HDL_Node (N))); + when N_True => + Put ("TRUE"); + when N_False => + Put ("FALSE"); + when N_EOS => + Put ("EOS"); + when N_Not_Bool => + Put ("!"); + Print_Expr (Get_Boolean (N), Prio); + when N_And_Bool => + Print_Expr (Get_Left (N), Prio); + Put (" && "); + Print_Expr (Get_Right (N), Prio); + when N_Or_Bool => + Print_Expr (Get_Left (N), Prio); + Put (" || "); + Print_Expr (Get_Right (N), Prio); + when N_Imp_Bool => + Print_Expr (Get_Left (N), Prio); + Put (" -> "); + Print_Expr (Get_Right (N), Prio); + when others => + Error_Kind ("print_expr", N); + end case; + if Prio < Parent_Prio then + Put (")"); + end if; + end Print_Expr; + + procedure Print_Sequence (Seq : Node; Parent_Prio : Priority); + + procedure Print_Count (N : Node) is + B : Node; + begin + B := Get_Low_Bound (N); + if B = Null_Node then + return; + end if; + Print_Expr (B); + B := Get_High_Bound (N); + if B = Null_Node then + return; + end if; + Put (":"); + Print_Expr (B); + end Print_Count; + + procedure Print_Binary_Sequence (Name : String; N : Node; Prio : Priority) + is + begin + Print_Sequence (Get_Left (N), Prio); + Put (Name); + Print_Sequence (Get_Right (N), Prio); + end Print_Binary_Sequence; + + procedure Print_Repeat_Sequence (Name : String; N : Node) is + S : Node; + begin + S := Get_Sequence (N); + if S /= Null_Node then + Print_Sequence (S, Prio_SERE_Repeat); + end if; + Put (Name); + Print_Count (N); + Put ("]"); + end Print_Repeat_Sequence; + + procedure Print_Sequence (Seq : Node; Parent_Prio : Priority) + is + Prio : constant Priority := Get_Priority (Seq); + Add_Paren : constant Boolean := Prio < Parent_Prio + or else Parent_Prio <= Prio_FL_Paren; + begin + if Add_Paren then + Put ("{"); + end if; + case Get_Kind (Seq) is + when N_Braced_SERE => + Put ("{"); + Print_Sequence (Get_SERE (Seq), Prio_Lowest); + Put ("}"); + when N_Concat_SERE => + Print_Binary_Sequence (";", Seq, Prio); + when N_Fusion_SERE => + Print_Binary_Sequence (":", Seq, Prio); + when N_Within_SERE => + Print_Binary_Sequence (" within ", Seq, Prio); + when N_Match_And_Seq => + Print_Binary_Sequence (" && ", Seq, Prio); + when N_Or_Seq => + Print_Binary_Sequence (" | ", Seq, Prio); + when N_And_Seq => + Print_Binary_Sequence (" & ", Seq, Prio); + when N_Star_Repeat_Seq => + Print_Repeat_Sequence ("[*", Seq); + when N_Goto_Repeat_Seq => + Print_Repeat_Sequence ("[->", Seq); + when N_Equal_Repeat_Seq => + Print_Repeat_Sequence ("[=", Seq); + when N_Plus_Repeat_Seq => + Print_Sequence (Get_Sequence (Seq), Prio); + Put ("[+]"); + when N_Booleans + | N_Name_Decl => + Print_Expr (Seq); + when others => + Error_Kind ("print_sequence", Seq); + end case; + if Add_Paren then + Put ("}"); + end if; + end Print_Sequence; + + procedure Print_Binary_Property (Name : String; N : Node; Prio : Priority) + is + begin + Print_Property (Get_Left (N), Prio); + Put (Name); + Print_Property (Get_Right (N), Prio); + end Print_Binary_Property; + + procedure Print_Binary_Property_SI (Name : String; + N : Node; Prio : Priority) + is + begin + Print_Property (Get_Left (N), Prio); + Put (Name); + if Get_Strong_Flag (N) then + Put ('!'); + end if; + if Get_Inclusive_Flag (N) then + Put ('_'); + end if; + Put (' '); + Print_Property (Get_Right (N), Prio); + end Print_Binary_Property_SI; + + procedure Print_Range_Property (Name : String; N : Node) is + begin + Put (Name); + Put ("["); + Print_Count (N); + Put ("]("); + Print_Property (Get_Property (N), Prio_FL_Paren); + Put (")"); + end Print_Range_Property; + + procedure Print_Boolean_Range_Property (Name : String; N : Node) is + begin + Put (Name); + Put ("("); + Print_Expr (Get_Boolean (N)); + Put (")["); + Print_Count (N); + Put ("]("); + Print_Property (Get_Property (N), Prio_FL_Paren); + Put (")"); + end Print_Boolean_Range_Property; + + procedure Print_Property (Prop : Node; + Parent_Prio : Priority := Prio_Lowest) + is + Prio : constant Priority := Get_Priority (Prop); + begin + if Prio < Parent_Prio then + Put ("("); + end if; + case Get_Kind (Prop) is + when N_Never => + Put ("never "); + Print_Property (Get_Property (Prop), Prio); + when N_Always => + Put ("always ("); + Print_Property (Get_Property (Prop), Prio); + Put (")"); + when N_Eventually => + Put ("eventually! ("); + Print_Property (Get_Property (Prop), Prio); + Put (")"); + when N_Strong => + Print_Property (Get_Property (Prop), Prio); + Put ("!"); + when N_Next => + Put ("next"); +-- if Get_Strong_Flag (Prop) then +-- Put ('!'); +-- end if; + Put (" ("); + Print_Property (Get_Property (Prop), Prio); + Put (")"); + when N_Next_A => + Print_Range_Property ("next_a", Prop); + when N_Next_E => + Print_Range_Property ("next_e", Prop); + when N_Next_Event => + Put ("next_event"); + Put ("("); + Print_Expr (Get_Boolean (Prop)); + Put (")("); + Print_Property (Get_Property (Prop), Prio); + Put (")"); + when N_Next_Event_A => + Print_Boolean_Range_Property ("next_event_a", Prop); + when N_Next_Event_E => + Print_Boolean_Range_Property ("next_event_e", Prop); + when N_Until => + Print_Binary_Property_SI (" until", Prop, Prio); + when N_Abort => + Print_Property (Get_Property (Prop), Prio); + Put (" abort "); + Print_Expr (Get_Boolean (Prop)); + when N_Before => + Print_Binary_Property_SI (" before", Prop, Prio); + when N_Or_Prop => + Print_Binary_Property (" || ", Prop, Prio); + when N_And_Prop => + Print_Binary_Property (" && ", Prop, Prio); + when N_Imp_Seq => + Print_Property (Get_Sequence (Prop), Prio); + Put (" |=> "); + Print_Property (Get_Property (Prop), Prio); + when N_Overlap_Imp_Seq => + Print_Property (Get_Sequence (Prop), Prio); + Put (" |-> "); + Print_Property (Get_Property (Prop), Prio); + when N_Log_Imp_Prop => + Print_Binary_Property (" -> ", Prop, Prio); + when N_Booleans + | N_Name_Decl => + Print_Expr (Prop); + when N_Sequences => + Print_Sequence (Prop, Parent_Prio); + when others => + Error_Kind ("print_property", Prop); + end case; + if Prio < Parent_Prio then + Put (")"); + end if; + end Print_Property; + + procedure Print_Assert (N : Node) is + Label : Name_Id; + begin + Put (" "); + Label := Get_Label (N); + if Label /= Null_Identifier then + Put (Image (Label)); + Put (": "); + end if; + Put ("assert "); + Print_Property (Get_Property (N)); + Put_Line (";"); + end Print_Assert; + + procedure Print_Property_Declaration (N : Node) is + begin + Put (" "); + Put ("property "); + Put (Image (Get_Identifier (N))); + Put (" = "); + Print_Property (Get_Property (N)); + Put_Line (";"); + end Print_Property_Declaration; + + procedure Print_Unit (Unit : Node) is + Item : Node; + begin + case Get_Kind (Unit) is + when N_Vunit => + Put ("vunit"); + when others => + Error_Kind ("disp_unit", Unit); + end case; + Put (' '); + Put (Image (Get_Identifier (Unit))); + Put_Line (" {"); + Item := Get_Item_Chain (Unit); + while Item /= Null_Node loop + case Get_Kind (Item) is + when N_Name_Decl => + null; + when N_Assert_Directive => + Print_Assert (Item); + when N_Property_Declaration => + Print_Property_Declaration (Item); + when others => + Error_Kind ("disp_unit", Item); + end case; + Item := Get_Chain (Item); + end loop; + Put_Line ("}"); + end Print_Unit; +end PSL.Prints; + diff --git a/src/psl/psl-prints.ads b/src/psl/psl-prints.ads new file mode 100644 index 000000000..18a36f78f --- /dev/null +++ b/src/psl/psl-prints.ads @@ -0,0 +1,20 @@ +with PSL.Nodes; use PSL.Nodes; +with PSL.Priorities; use PSL.Priorities; + +package PSL.Prints is + procedure Print_Unit (Unit : Node); + procedure Print_Property (Prop : Node; + Parent_Prio : Priority := Prio_Lowest); + procedure Print_Expr (N : Node; Parent_Prio : Priority := Prio_Lowest); + + -- Procedure to display HDL_Expr nodes. + type HDL_Expr_Printer_Acc is access procedure (N : HDL_Node); + HDL_Expr_Printer : HDL_Expr_Printer_Acc; + + procedure Print_HDL_Expr (N : HDL_Node); + + -- Like Print_Expr but always put parenthesis. + procedure Dump_Expr (N : Node); + +end PSL.Prints; + diff --git a/src/psl/psl-priorities.ads b/src/psl/psl-priorities.ads new file mode 100644 index 000000000..cb49239e4 --- /dev/null +++ b/src/psl/psl-priorities.ads @@ -0,0 +1,63 @@ +package PSL.Priorities is + -- Operator priorities, defined by PSL1.1 4.2.3.2 + type Priority is + ( + Prio_Lowest, + + -- always, never, G + Prio_FL_Invariance, + + -- ->, <-> + Prio_Bool_Imp, + + -- |->, |=> + Prio_Seq_Imp, + + -- U, W, until*, before* + Prio_FL_Bounding, + + -- next*, eventually!, X, X!, F + Prio_FL_Occurence, + + -- abort + Prio_FL_Abort, + + -- ( ) + Prio_FL_Paren, + + -- ; + Prio_Seq_Concat, + + -- : + Prio_Seq_Fusion, + + -- | + Prio_Seq_Or, + + -- &, && + Prio_Seq_And, + + -- within + Prio_Seq_Within, + + -- [*], [+], [=], [->] + Prio_SERE_Repeat, + + -- { } + Prio_SERE_Brace, + + -- @ + Prio_Clock_Event, + + -- ! + Prio_Strong, + + -- union + Prio_Union, + + -- ! + Prio_Bool_Not, + + Prio_HDL + ); +end PSL.Priorities; diff --git a/src/psl/psl-qm.adb b/src/psl/psl-qm.adb new file mode 100644 index 000000000..f5b5e1db3 --- /dev/null +++ b/src/psl/psl-qm.adb @@ -0,0 +1,318 @@ +with Ada.Text_IO; +with Types; use Types; +with PSL.Errors; use PSL.Errors; +with PSL.Prints; +with PSL.CSE; + +package body PSL.QM is + procedure Reset is + begin + for I in 1 .. Nbr_Terms loop + Set_HDL_Index (Term_Assoc (I), 0); + end loop; + Nbr_Terms := 0; + Term_Assoc := (others => Null_Node); + end Reset; + + function Term (P : Natural) return Vector_Type is + begin + return Shift_Left (1, P - 1); + end Term; + + procedure Disp_Primes_Set (Ps : Primes_Set) + is + use Ada.Text_IO; + use PSL.Prints; + Prime : Prime_Type; + T : Vector_Type; + First_Term : Boolean; + begin + if Ps.Nbr = 0 then + Put ("FALSE"); + return; + end if; + for I in 1 .. Ps.Nbr loop + Prime := Ps.Set (I); + if I /= 1 then + Put (" | "); + end if; + if Prime.Set = 0 then + Put ("TRUE"); + else + First_Term := True; + for J in 1 .. Max_Terms loop + T := Term (J); + if (Prime.Set and T) /= 0 then + if First_Term then + First_Term := False; + else + Put ('.'); + end if; + if (Prime.Val and T) = 0 then + Put ('!'); + end if; + Print_Expr (Term_Assoc (J)); + end if; + end loop; + end if; + end loop; + end Disp_Primes_Set; + + -- Return TRUE iff L includes R, ie + -- for all x, x in L => x in R. + function Included (L, R : Prime_Type) return Boolean is + begin + return ((L.Set or R.Set) = L.Set) + and then ((L.Val and R.Set) = (R.Val and R.Set)); + end Included; + + -- Return TRUE iff L and R have the same don't care set + -- and L and R can be merged into a new prime with a new don't care. + function Is_One_Change_Same (L, R : Prime_Type) return Boolean + is + V : Vector_Type; + begin + if L.Set /= R.Set then + return False; + end if; + V := L.Val xor R.Val; + return (V and -V) = V; + end Is_One_Change_Same; + + -- Return true iff L can add a new DC in R. + function Is_One_Change (L, R : Prime_Type) return Boolean + is + V : Vector_Type; + begin + if (L.Set or R.Set) /= R.Set then + return False; + end if; + V := (L.Val xor R.Val) and L.Set; + return (V and -V) = V; + end Is_One_Change; + + procedure Merge (Ps : in out Primes_Set; P : Prime_Type) + is + Do_Append : Boolean := True; + T : Prime_Type; + begin + for I in 1 .. Ps.Nbr loop + T := Ps.Set (I); + if Included (P, T) then + -- Already in the set. + return; + end if; + if Included (T, P) then + Ps.Set (I) := P; + Do_Append := False; + else + if Is_One_Change_Same (P, T) then + declare + V : constant Vector_Type := T.Val xor P.Val; + begin + Ps.Set (I).Set := T.Set and not V; + Ps.Set (I).Val := T.Val and not V; + end; + Do_Append := False; + end if; + if Is_One_Change (P, T) then + declare + V : constant Vector_Type := (T.Val xor P.Val) and P.Set; + begin + Ps.Set (I).Set := T.Set and not V; + Ps.Set (I).Val := T.Val and not V; + end; + -- continue. + end if; + end if; + end loop; + if Do_Append then + Ps.Nbr := Ps.Nbr + 1; + Ps.Set (Ps.Nbr) := P; + end if; + end Merge; + + function Build_Primes_And (L, R : Primes_Set) return Primes_Set + is + Res : Primes_Set (L.Nbr * R.Nbr); + L_P, R_P : Prime_Type; + P : Prime_Type; + begin + for I in 1 .. L.Nbr loop + L_P := L.Set (I); + for J in 1 .. R.Nbr loop + R_P := R.Set (J); + -- In case of conflict, discard. + if ((L_P.Val xor R_P.Val) and (L_P.Set and R_P.Set)) /= 0 then + null; + else + P.Set := L_P.Set or R_P.Set; + P.Val := (R_P.Set and R_P.Val) + or ((L_P.Set and not R_P.Set) and L_P.Val); + Merge (Res, P); + end if; + end loop; + end loop; + + return Res; + end Build_Primes_And; + + + function Build_Primes_Or (L, R : Primes_Set) return Primes_Set + is + Res : Primes_Set (L.Nbr + R.Nbr); + L_P, R_P : Prime_Type; + begin + for I in 1 .. L.Nbr loop + L_P := L.Set (I); + Merge (Res, L_P); + end loop; + for J in 1 .. R.Nbr loop + R_P := R.Set (J); + Merge (Res, R_P); + end loop; + + return Res; + end Build_Primes_Or; + + function Build_Primes (N : Node; Negate : Boolean) return Primes_Set is + begin + case Get_Kind (N) is + when N_HDL_Expr + | N_EOS => + declare + Res : Primes_Set (1); + Index : Int32; + T : Vector_Type; + begin + Index := Get_HDL_Index (N); + if Index = 0 then + Nbr_Terms := Nbr_Terms + 1; + if Nbr_Terms > Max_Terms then + raise Program_Error; + end if; + Term_Assoc (Nbr_Terms) := N; + Index := Int32 (Nbr_Terms); + Set_HDL_Index (N, Index); + else + if Index not in 1 .. Int32 (Nbr_Terms) + or else Term_Assoc (Natural (Index)) /= N + then + raise Internal_Error; + end if; + end if; + T := Term (Natural (Index)); + Res.Nbr := 1; + Res.Set (1).Set := T; + if Negate then + Res.Set (1).Val := 0; + else + Res.Set (1).Val := T; + end if; + return Res; + end; + when N_False => + declare + Res : Primes_Set (0); + begin + return Res; + end; + when N_True => + declare + Res : Primes_Set (1); + begin + Res.Nbr := 1; + Res.Set (1).Set := 0; + Res.Set (1).Val := 0; + return Res; + end; + when N_Not_Bool => + return Build_Primes (Get_Boolean (N), not Negate); + when N_And_Bool => + if Negate then + -- !(a & b) <-> !a || !b + return Build_Primes_Or (Build_Primes (Get_Left (N), True), + Build_Primes (Get_Right (N), True)); + else + return Build_Primes_And (Build_Primes (Get_Left (N), False), + Build_Primes (Get_Right (N), False)); + end if; + when N_Or_Bool => + if Negate then + -- !(a || b) <-> !a && !b + return Build_Primes_And (Build_Primes (Get_Left (N), True), + Build_Primes (Get_Right (N), True)); + else + return Build_Primes_Or (Build_Primes (Get_Left (N), False), + Build_Primes (Get_Right (N), False)); + end if; + when N_Imp_Bool => + if not Negate then + -- a -> b <-> !a || b + return Build_Primes_Or (Build_Primes (Get_Left (N), True), + Build_Primes (Get_Right (N), False)); + else + -- !(a -> b) <-> a && !b + return Build_Primes_And (Build_Primes (Get_Left (N), False), + Build_Primes (Get_Right (N), True)); + end if; + when others => + Error_Kind ("build_primes", N); + end case; + end Build_Primes; + + function Build_Primes (N : Node) return Primes_Set is + begin + return Build_Primes (N, False); + end Build_Primes; + + function Build_Node (P : Prime_Type) return Node + is + Res : Node := Null_Node; + N : Node; + S : Vector_Type := P.Set; + T : Vector_Type; + begin + if S = 0 then + return True_Node; + end if; + for I in Natural range 1 .. Vector_Type'Modulus loop + T := Term (I); + if (S and T) /= 0 then + N := Term_Assoc (I); + if (P.Val and T) = 0 then + N := PSL.CSE.Build_Bool_Not (N); + end if; + if Res = Null_Node then + Res := N; + else + Res := PSL.CSE.Build_Bool_And (Res, N); + end if; + S := S and not T; + exit when S = 0; + end if; + end loop; + return Res; + end Build_Node; + + function Build_Node (Ps : Primes_Set) return Node + is + Res : Node; + begin + if Ps.Nbr = 0 then + return False_Node; + else + Res := Build_Node (Ps.Set (1)); + for I in 2 .. Ps.Nbr loop + Res := PSL.CSE.Build_Bool_Or (Res, Build_Node (Ps.Set (I))); + end loop; + return Res; + end if; + end Build_Node; + + -- FIXME: finish the work: do a real Quine-McKluskey minimization. + function Reduce (N : Node) return Node is + begin + return Build_Node (Build_Primes (N)); + end Reduce; +end PSL.QM; diff --git a/src/psl/psl-qm.ads b/src/psl/psl-qm.ads new file mode 100644 index 000000000..85f1e3cf4 --- /dev/null +++ b/src/psl/psl-qm.ads @@ -0,0 +1,49 @@ +with PSL.Nodes; use PSL.Nodes; +with Interfaces; use Interfaces; + +package PSL.QM is + type Primes_Set (<>) is private; + + function Build_Primes (N : Node) return Primes_Set; + + function Build_Node (Ps : Primes_Set) return Node; + + function Reduce (N : Node) return Node; + + -- The maximum number of terms that this package can handle. + -- The algorithm is in O(2**n) + Max_Terms : constant Natural := 12; + + type Term_Assoc_Type is array (1 .. Max_Terms) of Node; + Term_Assoc : Term_Assoc_Type := (others => Null_Node); + Nbr_Terms : Natural := 0; + + procedure Reset; + + procedure Disp_Primes_Set (Ps : Primes_Set); +private + -- Scalar type used to represent a vector of booleans for terms. + subtype Vector_Type is Unsigned_16; + pragma Assert (Vector_Type'Modulus >= 2 ** Max_Terms); + + -- States of a vector of term. + -- If SET is 0, this is a don't care: the term has no influence. + -- If SET is 1, the value of the term is in VAL. + type Prime_Type is record + Val : Unsigned_16; + Set : Unsigned_16; + end record; + + subtype Len_Type is Natural range 0 .. 2 ** Max_Terms; + + type Set_Type is array (Natural range <>) of Prime_Type; + + -- A set of primes is a collection of at most MAX prime. + type Primes_Set (Max : Len_Type) is record + Nbr : Len_Type := 0; + Set : Set_Type (1 .. Max); + end record; +end PSL.QM; + + + diff --git a/src/psl/psl-rewrites.adb b/src/psl/psl-rewrites.adb new file mode 100644 index 000000000..6ba5b1026 --- /dev/null +++ b/src/psl/psl-rewrites.adb @@ -0,0 +1,604 @@ +with Types; use Types; +with PSL.Errors; use PSL.Errors; +with PSL.CSE; use PSL.CSE; + +package body PSL.Rewrites is +-- procedure Location_Copy (Dst, Src : Node) is +-- begin +-- Set_Location (Dst, Get_Location (Src)); +-- end Location_Copy; + + -- Return [*0] + function Build_Empty return Node is + Res, Tmp : Node; + begin + Res := Create_Node (N_Star_Repeat_Seq); + Tmp := Create_Node (N_Number); + Set_Value (Tmp, 0); + Set_Low_Bound (Res, Tmp); + return Res; + end Build_Empty; + + -- Return N[*] + function Build_Star (N : Node) return Node is + Res : Node; + begin + Res := Create_Node (N_Star_Repeat_Seq); + Set_Sequence (Res, N); + return Res; + end Build_Star; + + -- Return N[+] + function Build_Plus (N : Node) return Node is + Res : Node; + begin + Res := Create_Node (N_Plus_Repeat_Seq); + Set_Sequence (Res, N); + return Res; + end Build_Plus; + + -- Return N! + function Build_Strong (N : Node) return Node is + Res : Node; + begin + Res := Create_Node (N_Strong); + Set_Property (Res, N); + return Res; + end Build_Strong; + + -- Return T[*] + function Build_True_Star return Node is + begin + return Build_Star (True_Node); + end Build_True_Star; + + function Build_Binary (K : Nkind; L, R : Node) return Node is + Res : Node; + begin + Res := Create_Node (K); + Set_Left (Res, L); + Set_Right (Res, R); + return Res; + end Build_Binary; + + function Build_Concat (L, R : Node) return Node is + begin + return Build_Binary (N_Concat_SERE, L, R); + end Build_Concat; + + function Build_Repeat (N : Node; Cnt : Uns32) return Node is + Res : Node; + begin + if Cnt = 0 then + raise Internal_Error; + end if; + Res := N; + for I in 2 .. Cnt loop + Res := Build_Concat (Res, N); + end loop; + return Res; + end Build_Repeat; + + function Build_Overlap_Imp_Seq (S : Node; P : Node) return Node + is + Res : Node; + begin + Res := Create_Node (N_Overlap_Imp_Seq); + Set_Sequence (Res, S); + Set_Property (Res, P); + return Res; + end Build_Overlap_Imp_Seq; + + function Rewrite_Boolean (N : Node) return Node + is + Res : Node; + begin + case Get_Kind (N) is + when N_Name => + Res := Get_Decl (N); + pragma Assert (Res /= Null_Node); + return Res; + when N_Not_Bool => + Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); + return N; + when N_And_Bool + | N_Or_Bool + | N_Imp_Bool => + Set_Left (N, Rewrite_Boolean (Get_Left (N))); + Set_Right (N, Rewrite_Boolean (Get_Right (N))); + return N; + when N_HDL_Expr => + return N; + when others => + Error_Kind ("rewrite_boolean", N); + end case; + end Rewrite_Boolean; + + function Rewrite_Star_Repeat_Seq (Seq : Node; + Lo, Hi : Uns32) return Node + is + Res : Node; + begin + pragma Assert (Lo <= Hi); + + if Lo = Hi then + + if Lo = 0 then + -- r[*0] --> [*0] + return Build_Empty; + elsif Lo = 1 then + -- r[*1] --> r + return Seq; + end if; + -- r[*c+] --> r;r;r...;r (c times) + return Build_Repeat (Seq, Lo); + end if; + + -- r[*0:1] --> [*0] | r + -- r[*0:2] --> [*0] | r;{[*0]|r} + + -- r[*0:n] --> [*0] | r;r[*0:n-1] + -- r[*l:h] --> r[*l] ; r[*0:h-l] + Res := Build_Binary (N_Or_Seq, Build_Empty, Seq); + for I in Lo + 2 .. Hi loop + Res := Build_Concat (Seq, Res); + Res := Build_Binary (N_Or_Seq, Build_Empty, Res); + end loop; + if Lo > 0 then + Res := Build_Concat (Build_Repeat (Seq, Lo), Res); + end if; + + return Res; + end Rewrite_Star_Repeat_Seq; + + function Rewrite_Star_Repeat_Seq (Seq : Node; + Lo, Hi : Node) return Node + is + Cnt_Lo : Uns32; + Cnt_Hi : Uns32; + begin + if Lo = Null_Node then + -- r[*] + raise Program_Error; + end if; + + Cnt_Lo := Get_Value (Lo); + if Hi = Null_Node then + Cnt_Hi := Cnt_Lo; + else + Cnt_Hi := Get_Value (Hi); + end if; + return Rewrite_Star_Repeat_Seq (Seq, Cnt_Lo, Cnt_Hi); + end Rewrite_Star_Repeat_Seq; + + function Rewrite_Star_Repeat_Seq (N : Node) return Node + is + Seq : constant Node := Get_Sequence (N); + Lo : constant Node := Get_Low_Bound (N); + begin + if Lo = Null_Node then + -- r[*] --> r[*] + return N; + else + return Rewrite_Star_Repeat_Seq (Seq, Lo, Get_High_Bound (N)); + end if; + end Rewrite_Star_Repeat_Seq; + + function Rewrite_Goto_Repeat_Seq (Seq : Node; + Lo, Hi : Node) return Node is + Res : Node; + begin + -- b[->] --> {(~b)[*];b} + Res := Build_Concat (Build_Star (Build_Bool_Not (Seq)), Seq); + + if Lo = Null_Node then + return Res; + end if; + + -- b[->l:h] --> {b[->]}[*l:h] + return Rewrite_Star_Repeat_Seq (Res, Lo, Hi); + end Rewrite_Goto_Repeat_Seq; + + function Rewrite_Goto_Repeat_Seq (Seq : Node; + Lo, Hi : Uns32) return Node is + Res : Node; + begin + -- b[->] --> {(~b)[*];b} + Res := Build_Concat (Build_Star (Build_Bool_Not (Seq)), Seq); + + -- b[->l:h] --> {b[->]}[*l:h] + return Rewrite_Star_Repeat_Seq (Res, Lo, Hi); + end Rewrite_Goto_Repeat_Seq; + + function Rewrite_Equal_Repeat_Seq (N : Node) return Node + is + Seq : constant Node := Get_Sequence (N); + Lo : constant Node := Get_Low_Bound (N); + Hi : constant Node := Get_High_Bound (N); + begin + -- b[=l:h] --> {b[->l:h]};(~b)[*] + return Build_Concat (Rewrite_Goto_Repeat_Seq (Seq, Lo, Hi), + Build_Star (Build_Bool_Not (Seq))); + end Rewrite_Equal_Repeat_Seq; + + function Rewrite_Within (N : Node) return Node is + Res : Node; + begin + Res := Build_Concat (Build_Concat (Build_True_Star, Get_Left (N)), + Build_True_Star); + return Build_Binary (N_Match_And_Seq, Res, Get_Right (N)); + end Rewrite_Within; + + function Rewrite_And_Seq (L : Node; R : Node) return Node is + begin + return Build_Binary (N_Or_Seq, + Build_Binary (N_Match_And_Seq, + L, + Build_Concat (R, Build_True_Star)), + Build_Binary (N_Match_And_Seq, + Build_Concat (L, Build_True_Star), + R)); + end Rewrite_And_Seq; + pragma Unreferenced (Rewrite_And_Seq); + + procedure Rewrite_Instance (N : Node) + is + Assoc : Node := Get_Association_Chain (N); + begin + while Assoc /= Null_Node loop + case Get_Kind (Get_Formal (Assoc)) is + when N_Const_Parameter => + null; + when N_Boolean_Parameter => + Set_Actual (Assoc, Rewrite_Boolean (Get_Actual (Assoc))); + when N_Sequence_Parameter => + Set_Actual (Assoc, Rewrite_SERE (Get_Actual (Assoc))); + when N_Property_Parameter => + Set_Actual (Assoc, Rewrite_Property (Get_Actual (Assoc))); + when others => + Error_Kind ("rewrite_instance", + Get_Formal (Assoc)); + end case; + Assoc := Get_Chain (Assoc); + end loop; + end Rewrite_Instance; + + function Rewrite_SERE (N : Node) return Node is + S : Node; + begin + case Get_Kind (N) is + when N_Star_Repeat_Seq => + S := Get_Sequence (N); + if S = Null_Node then + S := True_Node; + else + S := Rewrite_SERE (S); + end if; + Set_Sequence (N, S); + return Rewrite_Star_Repeat_Seq (N); + when N_Plus_Repeat_Seq => + S := Get_Sequence (N); + if S = Null_Node then + S := True_Node; + else + S := Rewrite_SERE (S); + end if; + Set_Sequence (N, S); + return N; + when N_Goto_Repeat_Seq => + return Rewrite_Goto_Repeat_Seq + (Rewrite_SERE (Get_Sequence (N)), + Get_Low_Bound (N), Get_High_Bound (N)); + when N_Equal_Repeat_Seq => + Set_Sequence (N, Rewrite_SERE (Get_Sequence (N))); + return Rewrite_Equal_Repeat_Seq (N); + when N_Braced_SERE => + return Rewrite_SERE (Get_SERE (N)); + when N_Within_SERE => + Set_Left (N, Rewrite_SERE (Get_Left (N))); + Set_Right (N, Rewrite_SERE (Get_Right (N))); + return Rewrite_Within (N); +-- when N_And_Seq => +-- return Rewrite_And_Seq (Rewrite_SERE (Get_Left (N)), +-- Rewrite_SERE (Get_Right (N))); + when N_Concat_SERE + | N_Fusion_SERE + | N_Match_And_Seq + | N_And_Seq + | N_Or_Seq => + Set_Left (N, Rewrite_SERE (Get_Left (N))); + Set_Right (N, Rewrite_SERE (Get_Right (N))); + return N; + when N_Booleans => + return Rewrite_Boolean (N); + when N_Name => + return Get_Decl (N); + when N_Sequence_Instance + | N_Endpoint_Instance => + Rewrite_Instance (N); + return N; + when N_Boolean_Parameter + | N_Sequence_Parameter + | N_Const_Parameter => + return N; + when others => + Error_Kind ("rewrite_SERE", N); + end case; + end Rewrite_SERE; + + function Rewrite_Until (N : Node) return Node + is + Res : Node; + B : Node; + L : Node; + S : Node; + begin + if Get_Inclusive_Flag (N) then + -- B1 until_ B2 --> {B1[+]:B2} + Res := Build_Binary (N_Fusion_SERE, + Build_Plus (Rewrite_Boolean (Get_Left (N))), + Rewrite_Boolean (Get_Right (N))); + if Get_Strong_Flag (N) then + Res := Build_Strong (Res); + end if; + else + -- P until B --> {(!B)[+]} |-> P + B := Rewrite_Boolean (Get_Right (N)); + L := Build_Plus (Build_Bool_Not (B)); + Res := Build_Overlap_Imp_Seq (L, Rewrite_Property (Get_Left (N))); + + if Get_Strong_Flag (N) then + -- p until! b --> (p until b) && ({b[->]}!) + S := Build_Strong + (Rewrite_Goto_Repeat_Seq (B, Null_Node, Null_Node)); + Res := Build_Binary (N_And_Prop, Res, S); + end if; + end if; + return Res; + end Rewrite_Until; + + function Rewrite_Next_Event_A (B : Node; + Lo, Hi : Uns32; + P : Node; + Strong : Boolean) return Node + is + Res : Node; + begin + Res := Rewrite_Goto_Repeat_Seq (B, Lo, Hi); + Res := Build_Overlap_Imp_Seq (Res, P); + + if Strong then + Res := Build_Binary + (N_And_Prop, + Res, + Build_Strong (Rewrite_Goto_Repeat_Seq (B, Lo, Lo))); + end if; + + return Res; + end Rewrite_Next_Event_A; + + function Rewrite_Next_Event (B : Node; + N : Uns32; + P : Node; + Strong : Boolean) return Node is + begin + return Rewrite_Next_Event_A (B, N, N, P, Strong); + end Rewrite_Next_Event; + + function Rewrite_Next_Event (B : Node; + Num : Node; + P : Node; + Strong : Boolean) return Node + is + N : Uns32; + begin + if Num = Null_Node then + N := 1; + else + N := Get_Value (Num); + end if; + return Rewrite_Next_Event (B, N, P, Strong); + end Rewrite_Next_Event; + + function Rewrite_Next (Num : Node; P : Node; Strong : Boolean) return Node + is + N : Uns32; + begin + if Num = Null_Node then + N := 1; + else + N := Get_Value (Num); + end if; + return Rewrite_Next_Event (True_Node, N + 1, P, Strong); + end Rewrite_Next; + + function Rewrite_Next_A (Lo, Hi : Uns32; + P : Node; Strong : Boolean) return Node + is + begin + return Rewrite_Next_Event_A (True_Node, Lo + 1, Hi + 1, P, Strong); + end Rewrite_Next_A; + + function Rewrite_Next_Event_E (B1 : Node; + Lo, Hi : Uns32; + B2 : Node; Strong : Boolean) return Node + is + Res : Node; + begin + Res := Build_Binary (N_Fusion_SERE, + Rewrite_Goto_Repeat_Seq (B1, Lo, Hi), + B2); + if Strong then + Res := Build_Strong (Res); + end if; + return Res; + end Rewrite_Next_Event_E; + + function Rewrite_Next_E (Lo, Hi : Uns32; + B : Node; Strong : Boolean) return Node + is + begin + return Rewrite_Next_Event_E (True_Node, Lo + 1, Hi + 1, B, Strong); + end Rewrite_Next_E; + + function Rewrite_Before (N : Node) return Node + is + Res : Node; + R : Node; + B1, B2 : Node; + N_B2 : Node; + begin + B1 := Rewrite_Boolean (Get_Left (N)); + B2 := Rewrite_Boolean (Get_Right (N)); + N_B2 := Build_Bool_Not (B2); + Res := Build_Star (Build_Bool_And (Build_Bool_Not (B1), N_B2)); + + if Get_Inclusive_Flag (N) then + R := B2; + else + R := Build_Bool_And (B1, N_B2); + end if; + Res := Build_Concat (Res, R); + if Get_Strong_Flag (N) then + Res := Build_Strong (Res); + end if; + return Res; + end Rewrite_Before; + + function Rewrite_Or (L, R : Node) return Node + is + B, P : Node; + begin + if Get_Kind (L) in N_Booleans then + if Get_Kind (R) in N_Booleans then + return Build_Bool_Or (L, R); + else + B := L; + P := R; + end if; + elsif Get_Kind (R) in N_Booleans then + B := R; + P := L; + else + -- Not in the simple subset. + raise Program_Error; + end if; + + -- B || P --> (~B) -> P + return Build_Binary (N_Log_Imp_Prop, Build_Bool_Not (B), P); + end Rewrite_Or; + + function Rewrite_Property (N : Node) return Node is + begin + case Get_Kind (N) is + when N_Star_Repeat_Seq + | N_Plus_Repeat_Seq + | N_Goto_Repeat_Seq + | N_Sequence_Instance + | N_Endpoint_Instance + | N_Braced_SERE => + return Rewrite_SERE (N); + when N_Imp_Seq + | N_Overlap_Imp_Seq => + Set_Sequence (N, Rewrite_Property (Get_Sequence (N))); + Set_Property (N, Rewrite_Property (Get_Property (N))); + return N; + when N_Log_Imp_Prop => + -- b -> p --> {b} |-> p + return Build_Overlap_Imp_Seq + (Rewrite_Boolean (Get_Left (N)), + Rewrite_Property (Get_Right (N))); + when N_Eventually => + return Build_Strong + (Build_Binary (N_Fusion_SERE, + Build_Plus (True_Node), + Rewrite_SERE (Get_Property (N)))); + when N_Until => + return Rewrite_Until (N); + when N_Next => + return Rewrite_Next (Get_Number (N), + Rewrite_Property (Get_Property (N)), + Get_Strong_Flag (N)); + when N_Next_Event => + return Rewrite_Next_Event (Rewrite_Boolean (Get_Boolean (N)), + Get_Number (N), + Rewrite_Property (Get_Property (N)), + Get_Strong_Flag (N)); + when N_Next_A => + return Rewrite_Next_A (Get_Value (Get_Low_Bound (N)), + Get_Value (Get_High_Bound (N)), + Rewrite_Property (Get_Property (N)), + Get_Strong_Flag (N)); + when N_Next_Event_A => + return Rewrite_Next_Event_A + (Rewrite_Boolean (Get_Boolean (N)), + Get_Value (Get_Low_Bound (N)), + Get_Value (Get_High_Bound (N)), + Rewrite_Property (Get_Property (N)), + Get_Strong_Flag (N)); + when N_Next_E => + return Rewrite_Next_E (Get_Value (Get_Low_Bound (N)), + Get_Value (Get_High_Bound (N)), + Rewrite_Property (Get_Property (N)), + Get_Strong_Flag (N)); + when N_Next_Event_E => + return Rewrite_Next_Event_E + (Rewrite_Boolean (Get_Boolean (N)), + Get_Value (Get_Low_Bound (N)), + Get_Value (Get_High_Bound (N)), + Rewrite_Property (Get_Property (N)), + Get_Strong_Flag (N)); + when N_Before => + return Rewrite_Before (N); + when N_Booleans => + return Rewrite_Boolean (N); + when N_Name => + return Get_Decl (N); + when N_Never + | N_Always + | N_Strong => + -- Fully handled by psl.build + Set_Property (N, Rewrite_Property (Get_Property (N))); + return N; + when N_Clock_Event => + Set_Property (N, Rewrite_Property (Get_Property (N))); + Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); + return N; + when N_And_Prop => + Set_Left (N, Rewrite_Property (Get_Left (N))); + Set_Right (N, Rewrite_Property (Get_Right (N))); + return N; + when N_Or_Prop => + return Rewrite_Or (Rewrite_Property (Get_Left (N)), + Rewrite_Property (Get_Right (N))); + when N_Abort => + Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); + Set_Property (N, Rewrite_Property (Get_Property (N))); + return N; + when N_Property_Instance => + Rewrite_Instance (N); + return N; + when others => + Error_Kind ("rewrite_property", N); + end case; + end Rewrite_Property; + + procedure Rewrite_Unit (N : Node) is + Item : Node; + begin + Item := Get_Item_Chain (N); + while Item /= Null_Node loop + case Get_Kind (Item) is + when N_Name_Decl => + null; + when N_Assert_Directive => + Set_Property (Item, Rewrite_Property (Get_Property (Item))); + when N_Property_Declaration => + Set_Property (Item, Rewrite_Property (Get_Property (Item))); + when others => + Error_Kind ("rewrite_unit", Item); + end case; + Item := Get_Chain (Item); + end loop; + end Rewrite_Unit; +end PSL.Rewrites; diff --git a/src/psl/psl-rewrites.ads b/src/psl/psl-rewrites.ads new file mode 100644 index 000000000..ac76b7805 --- /dev/null +++ b/src/psl/psl-rewrites.ads @@ -0,0 +1,7 @@ +with PSL.Nodes; use PSL.Nodes; + +package PSL.Rewrites is + function Rewrite_SERE (N : Node) return Node; + function Rewrite_Property (N : Node) return Node; + procedure Rewrite_Unit (N : Node); +end PSL.Rewrites; diff --git a/src/psl/psl-subsets.adb b/src/psl/psl-subsets.adb new file mode 100644 index 000000000..f322eafda --- /dev/null +++ b/src/psl/psl-subsets.adb @@ -0,0 +1,177 @@ +with PSL.Errors; use PSL.Errors; +with Types; use Types; + +package body PSL.Subsets is + procedure Check_Simple (N : Node) + is + begin + case Get_Kind (N) is + when N_Not_Bool => + if Get_Psl_Type (Get_Boolean (N)) /= Type_Boolean then + Error_Msg_Sem + ("operand of a negation operator must be a boolean", N); + end if; + when N_Never => + case Get_Psl_Type (Get_Property (N)) is + when Type_Sequence | Type_Boolean => + null; + when others => + Error_Msg_Sem ("operand of a 'never' operator must be " + & "a boolean or a sequence", N); + end case; + when N_Eventually => + case Get_Psl_Type (Get_Property (N)) is + when Type_Sequence | Type_Boolean => + null; + when others => + Error_Msg_Sem ("operand of an 'eventually!' operator must be" + & " a boolean or a sequence", N); + end case; + when N_And_Bool => + if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then + Error_Msg_Sem ("left-hand side operand of logical 'and' must be" + & " a boolean", N); + end if; + when N_Or_Bool => + if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then + Error_Msg_Sem ("left-hand side operand of logical 'or' must be" + & " a boolean", N); + end if; + when N_Log_Imp_Prop => + if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then + Error_Msg_Sem ("left-hand side operand of logical '->' must be" + & " a boolean", N); + end if; + -- FIXME: <-> + when N_Until => + if not Get_Inclusive_Flag (N) then + if Get_Psl_Type (Get_Right (N)) /= Type_Boolean then + Error_Msg_Sem ("right-hand side of a non-overlapping " + & "'until*' operator must be a boolean", N); + end if; + else + if Get_Psl_Type (Get_Right (N)) /= Type_Boolean + or else Get_Psl_Type (Get_Left (N)) /= Type_Boolean + then + Error_Msg_Sem ("both operands of an overlapping 'until*'" + & " operator are boolean", N); + end if; + end if; + when N_Before => + if Get_Psl_Type (Get_Right (N)) /= Type_Boolean + or else Get_Psl_Type (Get_Left (N)) /= Type_Boolean + then + Error_Msg_Sem ("both operands of a 'before*'" + & " operator are boolean", N); + end if; + when others => + null; + end case; + + -- Recursion. + case Get_Kind (N) is + when N_Error => + null; + when N_Hdl_Mod_Name => + null; + when N_Vunit + | N_Vmode + | N_Vprop => + declare + Item : Node; + begin + Item := Get_Item_Chain (N); + while Item /= Null_Node loop + Check_Simple (Item); + Item := Get_Chain (Item); + end loop; + end; + when N_Name_Decl => + null; + when N_Assert_Directive + | N_Property_Declaration => + Check_Simple (Get_Property (N)); + when N_Endpoint_Declaration + | N_Sequence_Declaration => + Check_Simple (Get_Sequence (N)); + when N_Clock_Event => + Check_Simple (Get_Property (N)); + Check_Simple (Get_Boolean (N)); + when N_Always + | N_Never + | N_Eventually + | N_Strong => + Check_Simple (Get_Property (N)); + when N_Braced_SERE => + Check_Simple (Get_SERE (N)); + when N_Concat_SERE + | N_Fusion_SERE + | N_Within_SERE => + Check_Simple (Get_Left (N)); + Check_Simple (Get_Right (N)); + when N_Name => + null; + when N_Star_Repeat_Seq + | N_Goto_Repeat_Seq + | N_Equal_Repeat_Seq => + declare + N2 : constant Node := Get_Sequence (N); + begin + if N2 /= Null_Node then + Check_Simple (N2); + end if; + end; + when N_Plus_Repeat_Seq => + Check_Simple (Get_Sequence (N)); + when N_Match_And_Seq + | N_And_Seq + | N_Or_Seq => + Check_Simple (Get_Left (N)); + Check_Simple (Get_Right (N)); + when N_Imp_Seq + | N_Overlap_Imp_Seq => + Check_Simple (Get_Sequence (N)); + Check_Simple (Get_Property (N)); + when N_Log_Imp_Prop + | N_Until + | N_Before + | N_Or_Prop + | N_And_Prop + | N_And_Bool + | N_Or_Bool + | N_Imp_Bool => + Check_Simple (Get_Left (N)); + Check_Simple (Get_Right (N)); + when N_Next + | N_Next_A + | N_Next_E => + Check_Simple (Get_Property (N)); + when N_Next_Event + | N_Next_Event_A + | N_Next_Event_E + | N_Abort => + Check_Simple (Get_Boolean (N)); + Check_Simple (Get_Property (N)); + when N_Not_Bool => + Check_Simple (Get_Boolean (N)); + when N_Const_Parameter + | N_Sequence_Parameter + | N_Boolean_Parameter + | N_Property_Parameter => + null; + when N_Actual => + null; + when N_Sequence_Instance + | N_Endpoint_Instance + | N_Property_Instance => + null; + when N_True + | N_False + | N_Number + | N_EOS + | N_HDL_Expr => + null; + end case; + end Check_Simple; +end PSL.Subsets; + diff --git a/src/psl/psl-subsets.ads b/src/psl/psl-subsets.ads new file mode 100644 index 000000000..c3bae09ef --- /dev/null +++ b/src/psl/psl-subsets.ads @@ -0,0 +1,23 @@ +with PSL.Nodes; use PSL.Nodes; + +package PSL.Subsets is + -- Check that N (a property) follows the simple subset rules from + -- PSL v1.1 4.4.4 Simple subset. + -- Ie: + -- - The operand of a negation operator is a Boolean. + -- - The operand of a 'never' operator is a Boolean or a Sequence. + -- - The operand of an 'eventually!' operator is a Boolean or a Sequence. + -- - The left-hand side operand of a logical 'and' operator is a Boolean. + -- - The left-hand side operand of a logical 'or' operator is a Boolean. + -- - The left-hand side operand of a logical implication '->' operator + -- is a Boolean. + -- - Both operands of a logical iff '<->' operator are Boolean. + -- - The right-hand side operand of a non-overlapping 'until*' operator is + -- a Boolean. + -- - Both operands of an overlapping 'until*' operator are Boolean. + -- - Both operands of a 'before*' operator are Boolean. + -- + -- All other operators not mentioned above are supported in the simple + -- subset without restriction. + procedure Check_Simple (N : Node); +end PSL.Subsets; diff --git a/src/psl/psl-tprint.adb b/src/psl/psl-tprint.adb new file mode 100644 index 000000000..eabe8bd28 --- /dev/null +++ b/src/psl/psl-tprint.adb @@ -0,0 +1,255 @@ +with Types; use Types; +with PSL.Errors; use PSL.Errors; +with PSL.Prints; +with Ada.Text_IO; use Ada.Text_IO; +with Name_Table; use Name_Table; + +package body PSL.Tprint is + procedure Disp_Expr (N : Node) is + begin + case Get_Kind (N) is + when N_Number => + declare + Str : constant String := Uns32'Image (Get_Value (N)); + begin + Put (Str (2 .. Str'Last)); + end; + when others => + Error_Kind ("disp_expr", N); + end case; + end Disp_Expr; + + procedure Disp_Count (N : Node) is + B : Node; + begin + B := Get_Low_Bound (N); + if B = Null_Node then + return; + end if; + Disp_Expr (B); + B := Get_High_Bound (N); + if B = Null_Node then + return; + end if; + Put (":"); + Disp_Expr (B); + end Disp_Count; + + procedure Put_Node (Prefix : String; Name : String) is + begin + Put (Prefix); + Put ("-+ "); + Put (Name); + end Put_Node; + + procedure Put_Node_Line (Prefix : String; Name : String) is + begin + Put_Node (Prefix, Name); + New_Line; + end Put_Node_Line; + + function Down (Str : String) return String is + L : constant Natural := Str'Last; + begin + if Str (L) = '\' then + return Str (Str'First .. L - 1) & " \"; + elsif Str (L) = '/' then + return Str (Str'First .. L - 1) & "| \"; + else + raise Program_Error; + end if; + end Down; + + function Up (Str : String) return String is + L : constant Natural := Str'Last; + begin + if Str (L) = '/' then + return Str (Str'First .. L - 1) & " /"; + elsif Str (L) = '\' then + return Str (Str'First .. L - 1) & "| /"; + else + raise Program_Error; + end if; + end Up; + + procedure Disp_Repeat_Sequence (Prefix : String; Name : String; N : Node) is + S : Node; + begin + Put_Node (Prefix, Name); + Disp_Count (N); + Put_Line ("]"); + S := Get_Sequence (N); + if S /= Null_Node then + Disp_Property (Down (Prefix), S); + end if; + end Disp_Repeat_Sequence; + + procedure Disp_Binary_Sequence (Prefix : String; Name : String; N : Node) is + begin + Disp_Property (Up (Prefix), Get_Left (N)); + Put_Node_Line (Prefix, Name); + Disp_Property (Down (Prefix), Get_Right (N)); + end Disp_Binary_Sequence; + + procedure Disp_Range_Property (Prefix : String; Name : String; N : Node) is + begin + Put_Node (Prefix, Name); + Put ("["); + Disp_Count (N); + Put_Line ("]"); + Disp_Property (Down (Prefix), Get_Property (N)); + end Disp_Range_Property; + + procedure Disp_Boolean_Range_Property (Prefix : String; + Name : String; N : Node) is + begin + Disp_Property (Up (Prefix), Get_Boolean (N)); + Put_Node (Prefix, Name); + Put ("["); + Disp_Count (N); + Put_Line ("]"); + Disp_Property (Down (Prefix), Get_Property (N)); + end Disp_Boolean_Range_Property; + + procedure Disp_Property (Prefix : String; Prop : Node) is + begin + case Get_Kind (Prop) is + when N_Never => + Put_Node_Line (Prefix, "never"); + Disp_Property (Down (Prefix), Get_Property (Prop)); + when N_Always => + Put_Node_Line (Prefix, "always"); + Disp_Property (Down (Prefix), Get_Property (Prop)); + when N_Eventually => + Put_Node_Line (Prefix, "eventually!"); + Disp_Property (Down (Prefix), Get_Property (Prop)); + when N_Next => + Put_Node_Line (Prefix, "next"); +-- if Get_Strong_Flag (Prop) then +-- Put ('!'); +-- end if; + Disp_Property (Down (Prefix), Get_Property (Prop)); + when N_Next_A => + Disp_Range_Property (Prefix, "next_a", Prop); + when N_Next_E => + Disp_Range_Property (Prefix, "next_e", Prop); + when N_Next_Event => + Disp_Property (Up (Prefix), Get_Boolean (Prop)); + Put_Node_Line (Prefix, "next_event"); + Disp_Property (Down (Prefix), Get_Property (Prop)); + when N_Next_Event_A => + Disp_Boolean_Range_Property (Prefix, "next_event_a", Prop); + when N_Next_Event_E => + Disp_Boolean_Range_Property (Prefix, "next_event_e", Prop); + when N_Braced_SERE => + Put_Node_Line (Prefix, "{} (braced_SERE)"); + Disp_Property (Down (Prefix), Get_SERE (Prop)); + when N_Concat_SERE => + Disp_Binary_Sequence (Prefix, "; (concat)", Prop); + when N_Fusion_SERE => + Disp_Binary_Sequence (Prefix, ": (fusion)", Prop); + when N_Within_SERE => + Disp_Binary_Sequence (Prefix, "within", Prop); + when N_Match_And_Seq => + Disp_Binary_Sequence (Prefix, "&& (sequence matching len)", Prop); + when N_Or_Seq => + Disp_Binary_Sequence (Prefix, "| (sequence or)", Prop); + when N_And_Seq => + Disp_Binary_Sequence (Prefix, "& (sequence and)", Prop); + when N_Imp_Seq => + Disp_Property (Up (Prefix), Get_Sequence (Prop)); + Put_Node_Line (Prefix, "|=> (sequence implication)"); + Disp_Property (Down (Prefix), Get_Property (Prop)); + when N_Overlap_Imp_Seq => + Disp_Property (Up (Prefix), Get_Sequence (Prop)); + Put_Node_Line (Prefix, "|->"); + Disp_Property (Down (Prefix), Get_Property (Prop)); + when N_Or_Prop => + Disp_Binary_Sequence (Prefix, "|| (property or)", Prop); + when N_And_Prop => + Disp_Binary_Sequence (Prefix, "&& (property and)", Prop); + when N_Log_Imp_Prop => + Disp_Binary_Sequence (Prefix, "-> (property impliciation)", Prop); + when N_Until => + Disp_Binary_Sequence (Prefix, "until", Prop); + when N_Before => + Disp_Binary_Sequence (Prefix, "before", Prop); + when N_Abort => + Disp_Property (Up (Prefix), Get_Property (Prop)); + Put_Node_Line (Prefix, "abort"); + Disp_Property (Down (Prefix), Get_Boolean (Prop)); + when N_Not_Bool => + Put_Node_Line (Prefix, "! (boolean not)"); + Disp_Property (Down (Prefix), Get_Boolean (Prop)); + when N_Or_Bool => + Disp_Binary_Sequence (Prefix, "|| (boolean or)", Prop); + when N_And_Bool => + Disp_Binary_Sequence (Prefix, "&& (boolean and)", Prop); + when N_Name_Decl => + Put_Node_Line (Prefix, + "Name_Decl: " & Image (Get_Identifier (Prop))); + when N_Name => + Put_Node_Line (Prefix, "Name: " & Image (Get_Identifier (Prop))); + Disp_Property (Down (Prefix), Get_Decl (Prop)); + when N_True => + Put_Node_Line (Prefix, "TRUE"); + when N_False => + Put_Node_Line (Prefix, "FALSE"); + when N_HDL_Expr => + Put_Node (Prefix, "HDL_Expr: "); + PSL.Prints.HDL_Expr_Printer.all (Get_HDL_Node (Prop)); + New_Line; + when N_Star_Repeat_Seq => + Disp_Repeat_Sequence (Prefix, "[*", Prop); + when N_Goto_Repeat_Seq => + Disp_Repeat_Sequence (Prefix, "[->", Prop); + when N_Equal_Repeat_Seq => + Disp_Repeat_Sequence (Prefix, "[=", Prop); + when N_Plus_Repeat_Seq => + Put_Node_Line (Prefix, "[+]"); + Disp_Property (Down (Prefix), Get_Sequence (Prop)); + when others => + Error_Kind ("disp_property", Prop); + end case; + end Disp_Property; + + procedure Disp_Assert (N : Node) is + Label : constant Name_Id := Get_Label (N); + begin + Put (" "); + if Label /= Null_Identifier then + Put (Image (Label)); + Put (": "); + end if; + Put_Line ("assert "); + Disp_Property (" \", Get_Property (N)); + end Disp_Assert; + + procedure Disp_Unit (Unit : Node) is + Item : Node; + begin + case Get_Kind (Unit) is + when N_Vunit => + Put ("vunit"); + when others => + Error_Kind ("disp_unit", Unit); + end case; + Put (' '); + Put (Image (Get_Identifier (Unit))); + Put_Line (" {"); + Item := Get_Item_Chain (Unit); + while Item /= Null_Node loop + case Get_Kind (Item) is + when N_Assert_Directive => + Disp_Assert (Item); + when N_Name_Decl => + null; + when others => + Error_Kind ("disp_unit", Item); + end case; + Item := Get_Chain (Item); + end loop; + Put_Line ("}"); + end Disp_Unit; +end PSL.Tprint; + diff --git a/src/psl/psl-tprint.ads b/src/psl/psl-tprint.ads new file mode 100644 index 000000000..1b06ebf1a --- /dev/null +++ b/src/psl/psl-tprint.ads @@ -0,0 +1,6 @@ +with PSL.Nodes; use PSL.Nodes; + +package PSL.Tprint is + procedure Disp_Unit (Unit : Node); + procedure Disp_Property (Prefix : String; Prop : Node); +end PSL.Tprint; diff --git a/src/psl/psl.ads b/src/psl/psl.ads new file mode 100644 index 000000000..a2f4bdce0 --- /dev/null +++ b/src/psl/psl.ads @@ -0,0 +1,3 @@ +package PSL is + pragma Pure (PSL); +end PSL; |