diff --git a/CHANGELOG b/CHANGELOG index 550e0233..4b0ca953 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -12,6 +12,7 @@ * SystemVerilog: package scope operator * SystemVerilog: checkers * SystemVerilog: clocking block declarations +* SystemVerilog: typedefs from package scopes # EBMC 5.4 diff --git a/regression/verilog/packages/package_typedef1.sv b/regression/verilog/packages/package_typedef1.sv index 26ec78ba..d43a9d11 100644 --- a/regression/verilog/packages/package_typedef1.sv +++ b/regression/verilog/packages/package_typedef1.sv @@ -10,6 +10,6 @@ module main; moo::my_type some_var; - assert final ($typename(some_var) == "byte"); + assert final ($typename(some_var) == "bit signed[7:0]"); endmodule diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 06bc91e4..900e0ba3 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -1546,10 +1546,13 @@ data_type: { init($$, ID_verilog_chandle); } | TOK_VIRTUAL interface_opt interface_identifier { init($$, "virtual_interface"); } - | /*scope_opt*/ type_identifier packed_dimension_brace - { stack_expr($1).id(ID_typedef_type); - add_as_subtype(stack_type($2), stack_type($1)); + | type_identifier packed_dimension_brace + { add_as_subtype(stack_type($2), stack_type($1)); $$ = $2; } + | package_scope type_identifier packed_dimension_brace + { mto($1, $2); + add_as_subtype(stack_type($3), stack_type($2)); + $$ = $3; } // | class_type | TOK_EVENT { init($$, ID_verilog_event); } diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp index bb5273b3..7da5e7d3 100644 --- a/src/verilog/verilog_elaborate_type.cpp +++ b/src/verilog/verilog_elaborate_type.cpp @@ -149,6 +149,42 @@ typet verilog_typecheck_exprt::convert_packed_array_type( /*******************************************************************\ +Function: verilog_typecheck_exprt::elaborate_package_scope_typedef + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet verilog_typecheck_exprt::elaborate_package_scope_typedef( + const type_with_subtypest &src) +{ + auto location = src.source_location(); + + if(src.subtypes()[1].id() != ID_typedef_type) + throw errort().with_location(location) + << "verilog_package_scope expects typedef_type on the rhs"; + + auto package_base_name = src.subtypes()[0].id(); + auto typedef_base_name = src.subtypes()[1].get(ID_base_name); + + // stitch together + irep_idt full_identifier = + id2string(verilog_package_identifier(package_base_name)) + '.' + + id2string(typedef_base_name); + + // recursive call + verilog_typedef_typet full_typedef_type(full_identifier); + full_typedef_type.set(ID_identifier, full_identifier); + + return elaborate_type(full_typedef_type); +} + +/*******************************************************************\ + Function: verilog_typecheck_exprt::elaborate_type Inputs: @@ -283,7 +319,7 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src) // Look it up! const symbolt *symbol_ptr; - auto identifier = src.get(ID_identifier); + auto identifier = to_verilog_typedef_type(src).identifier(); if(ns.lookup(identifier, symbol_ptr)) throw errort().with_location(source_location) @@ -402,6 +438,11 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src) { return src; } + else if(src.id() == ID_verilog_package_scope) + { + // package::typedef + return elaborate_package_scope_typedef(to_type_with_subtypes(src)); + } else { throw errort().with_location(source_location) diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h index 248db3ae..eae33ead 100644 --- a/src/verilog/verilog_typecheck_expr.h +++ b/src/verilog/verilog_typecheck_expr.h @@ -66,6 +66,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset void propagate_type(exprt &expr, const typet &type); typet elaborate_type(const typet &); + typet elaborate_package_scope_typedef(const type_with_subtypest &); typet convert_enum(const class verilog_enum_typet &); array_typet convert_unpacked_array_type(const type_with_subtypet &); typet convert_packed_array_type(const type_with_subtypet &); diff --git a/src/verilog/verilog_types.h b/src/verilog/verilog_types.h index d723839b..6149579b 100644 --- a/src/verilog/verilog_types.h +++ b/src/verilog/verilog_types.h @@ -618,4 +618,42 @@ inline verilog_event_typet &to_verilog_event_type(typet &type) return static_cast(type); } +/// A typedef +class verilog_typedef_typet : public typet +{ +public: + explicit verilog_typedef_typet(const irep_idt &_identifier) + : typet(ID_typedef_type) + { + identifier(_identifier); + } + + void identifier(const irep_idt &identifier) + { + set(ID_identifier, identifier); + } + + const irep_idt &identifier() const + { + return get(ID_identifier); + } +}; + +/// Cast a generic typet to a \ref verilog_typedef_typet. This is an unchecked +/// conversion. \a type must be known to be \ref verilog_typedef_typet. +/// \param type: Source type +/// \return Object of type \ref verilog_typedef_typet +inline const verilog_typedef_typet &to_verilog_typedef_type(const typet &type) +{ + PRECONDITION(type.id() == ID_typedef_type); + return static_cast(type); +} + +/// \copydoc to_verilog_typedef_type(const typet &) +inline verilog_typedef_typet &to_verilog_typedef_type(typet &type) +{ + PRECONDITION(type.id() == ID_typedef_type); + return static_cast(type); +} + #endif