diff options
Diffstat (limited to 'src/psl/psl-rewrites.adb')
| -rw-r--r-- | src/psl/psl-rewrites.adb | 604 |
1 files changed, 604 insertions, 0 deletions
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; |