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 + 7 files changed, 28 insertions(+), 7 deletions(-) (limited to 'src/psl') 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 => -- cgit v1.2.3