From 8e84ebdf517fde66db0659245b88319f4da25a72 Mon Sep 17 00:00:00 2001 From: Tristan Gingold Date: Thu, 26 Aug 2021 08:07:34 +0200 Subject: PSL: handle inf in star repeat sequence. Fix #1832 --- src/psl/psl-nodes.adb | 4 +++- src/psl/psl-nodes.adb.in | 3 ++- src/psl/psl-nodes.ads | 3 +++ src/psl/psl-nodes_meta.adb | 4 ++++ src/psl/psl-prints.adb | 6 +++++- src/psl/psl-rewrites.adb | 14 ++++++++++---- src/psl/psl-subsets.adb | 1 + src/vhdl/vhdl-parse_psl.adb | 16 ++++++++++++---- src/vhdl/vhdl-prints.adb | 4 ++++ 9 files changed, 44 insertions(+), 11 deletions(-) diff --git a/src/psl/psl-nodes.adb b/src/psl/psl-nodes.adb index 6d392150b..108dfe7b2 100644 --- a/src/psl/psl-nodes.adb +++ b/src/psl/psl-nodes.adb @@ -391,7 +391,8 @@ package body PSL.Nodes is | N_HDL_Bool => return Type_Boolean; when N_Number - | N_Const_Parameter => + | N_Const_Parameter + | N_Inf => return Type_Numeric; when N_Vmode | N_Vunit @@ -482,6 +483,7 @@ package body PSL.Nodes is | N_EOS | N_Name | N_Name_Decl + | N_Inf | N_Number => return Format_Short; end case; diff --git a/src/psl/psl-nodes.adb.in b/src/psl/psl-nodes.adb.in index 3bbb26538..a644ebb71 100644 --- a/src/psl/psl-nodes.adb.in +++ b/src/psl/psl-nodes.adb.in @@ -391,7 +391,8 @@ package body PSL.Nodes is | N_HDL_Bool => return Type_Boolean; when N_Number - | N_Const_Parameter => + | N_Const_Parameter + | N_Inf => return Type_Numeric; when N_Vmode | N_Vunit diff --git a/src/psl/psl-nodes.ads b/src/psl/psl-nodes.ads index 07d4f7df6..c92af81dc 100644 --- a/src/psl/psl-nodes.ads +++ b/src/psl/psl-nodes.ads @@ -99,6 +99,7 @@ package PSL.Nodes is N_Name, N_Name_Decl, + N_Inf, N_Number ); for Nkind'Size use 8; @@ -253,6 +254,8 @@ package PSL.Nodes is -- -- Get/Set_Chain (Field2) + -- N_Inf (Short) + -- N_Number (Short) -- -- Get/Set_Value (Field1) diff --git a/src/psl/psl-nodes_meta.adb b/src/psl/psl-nodes_meta.adb index 8486c177f..92d18b735 100644 --- a/src/psl/psl-nodes_meta.adb +++ b/src/psl/psl-nodes_meta.adb @@ -258,6 +258,8 @@ package body PSL.Nodes_Meta is return "name"; when N_Name_Decl => return "name_decl"; + when N_Inf => + return "inf"; when N_Number => return "number"; end case; @@ -574,6 +576,7 @@ package body PSL.Nodes_Meta is -- N_Name_Decl Field_Identifier, Field_Chain, + -- N_Inf -- N_Number Field_Value ); @@ -643,6 +646,7 @@ package body PSL.Nodes_Meta is N_EOS => 169, N_Name => 171, N_Name_Decl => 173, + N_Inf => 173, N_Number => 174 ); diff --git a/src/psl/psl-prints.adb b/src/psl/psl-prints.adb index c9b343760..e1beb27c2 100644 --- a/src/psl/psl-prints.adb +++ b/src/psl/psl-prints.adb @@ -24,7 +24,8 @@ package body PSL.Prints is function Get_Priority (N : Node) return Priority is begin case Get_Kind (N) is - when N_Never | N_Always => + when N_Never + | N_Always => return Prio_FL_Invariance; when N_Eventually | N_Next @@ -65,6 +66,7 @@ package body PSL.Prints is return Prio_Bool_Imp; when N_Name_Decl | N_Number + | N_Inf | N_True | N_False | N_EOS @@ -149,6 +151,8 @@ package body PSL.Prints is begin Put (Str (2 .. Str'Last)); end; + when N_Inf => + Put ("inf"); when N_Name_Decl => Put (Image (Get_Identifier (N))); when N_HDL_Expr diff --git a/src/psl/psl-rewrites.adb b/src/psl/psl-rewrites.adb index 7568ab8fc..d8d9d5ecb 100644 --- a/src/psl/psl-rewrites.adb +++ b/src/psl/psl-rewrites.adb @@ -161,14 +161,20 @@ package body PSL.Rewrites is Cnt_Lo : Uns32; Cnt_Hi : Uns32; begin - if Lo = Null_Node then - -- r[*] - raise Program_Error; - end if; + -- r[*] must have been handled. + pragma Assert (Lo /= Null_Node); Cnt_Lo := Get_Value (Lo); if Hi = Null_Node then Cnt_Hi := Cnt_Lo; + elsif Get_Kind (Hi) = N_Inf then + -- r[*N to inf] --> r[*N] ; r[*] + if Cnt_Lo = 0 then + return Build_Star (Seq); + else + return Build_Concat (Rewrite_Star_Repeat_Seq (Seq, Cnt_Lo, Cnt_Lo), + Build_Star (Seq)); + end if; else Cnt_Hi := Get_Value (Hi); end if; diff --git a/src/psl/psl-subsets.adb b/src/psl/psl-subsets.adb index d5e3c1985..303d01c1e 100644 --- a/src/psl/psl-subsets.adb +++ b/src/psl/psl-subsets.adb @@ -188,6 +188,7 @@ package body PSL.Subsets is when N_True | N_False | N_Number + | N_Inf | N_EOS | N_HDL_Expr | N_HDL_Bool => diff --git a/src/vhdl/vhdl-parse_psl.adb b/src/vhdl/vhdl-parse_psl.adb index 314249c14..808c2dae7 100644 --- a/src/vhdl/vhdl-parse_psl.adb +++ b/src/vhdl/vhdl-parse_psl.adb @@ -57,9 +57,9 @@ package body Vhdl.Parse_Psl is Scan; return Res; elsif Current_Token = Tok_Inf then - -- FIXME: create node + Res := Create_Node_Loc (N_Inf); Scan; - return Null_Node; + return Res; else Error_Msg_Parse ("number expected"); return Null_Node; @@ -68,9 +68,16 @@ package body Vhdl.Parse_Psl is procedure Check_Positive_Count (N : Node) is - Low : constant Uns32 := Get_Value (Get_Low_Bound (N)); - High : constant Uns32 := Get_Value (Get_High_Bound (N)); + Low_B : constant Node := Get_Low_Bound (N); + High_B : constant Node := Get_High_Bound (N); + Low : constant Uns32 := Get_Value (Low_B); + High : Uns32; begin + if Get_Kind (High_B) = N_Inf then + return; + end if; + + High := Get_Value (High_B); if Low > High then Error_Msg_Parse ("Low bound of range must be lower than High bound," & @@ -840,6 +847,7 @@ package body Vhdl.Parse_Psl is | N_False | N_True | N_Number + | N_Inf | N_Name_Decl | N_Name | N_EOS diff --git a/src/vhdl/vhdl-prints.adb b/src/vhdl/vhdl-prints.adb index 361cbe18b..ec4d870e5 100644 --- a/src/vhdl/vhdl-prints.adb +++ b/src/vhdl/vhdl-prints.adb @@ -1958,6 +1958,10 @@ package body Vhdl.Prints is Disp_Str (Ctxt, Str); Close_Lit (Ctxt); end; + when N_Inf => + Start_Lit (Ctxt, Tok_Identifier); + Disp_Str (Ctxt, "INF"); + Close_Lit (Ctxt); when N_Name_Decl => Disp_Ident (Ctxt, Get_Identifier (N)); when N_HDL_Expr -- cgit v1.2.3