diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 012deea56..0d4509bfd 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -127,6 +127,7 @@ IREP_ID_ONE(verilog_associative_array) IREP_ID_ONE(verilog_declarations) IREP_ID_ONE(verilog_default_clocking) IREP_ID_ONE(verilog_default_disable) +IREP_ID_ONE(verilog_identifier) IREP_ID_ONE(verilog_interconnect) IREP_ID_ONE(verilog_lifetime) IREP_ID_ONE(verilog_logical_equality) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 9d82f7a10..9f1de4eee 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -4768,6 +4768,7 @@ hierarchical_identifier: | hierarchical_identifier '.' identifier { init($$, ID_hierarchical_identifier); stack_expr($$).reserve_operands(2); + stack_expr($3).id(ID_verilog_identifier); mto($$, $1); mto($$, $3); } diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index f1b960086..04a4bbec7 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -11,6 +11,36 @@ Author: Daniel Kroening, kroening@kroening.com #include +/// A simple Verilog identifier, unqualified +class verilog_identifier_exprt : public nullary_exprt +{ +public: + const irep_idt &base_name() const + { + return get(ID_base_name); + } + + void identifier(irep_idt _base_name) + { + set(ID_base_name, _base_name); + } +}; + +inline const verilog_identifier_exprt & +to_verilog_identifier_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_verilog_identifier); + verilog_identifier_exprt::check(expr); + return static_cast(expr); +} + +inline verilog_identifier_exprt &to_verilog_identifier_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_verilog_identifier); + verilog_identifier_exprt::check(expr); + return static_cast(expr); +} + /// The syntax for these A.B, where A is a module identifier and B /// is an identifier within that module. B is given als symbol_exprt. class hierarchical_identifier_exprt : public binary_exprt @@ -21,12 +51,12 @@ class hierarchical_identifier_exprt : public binary_exprt return op0(); } - const symbol_exprt &item() const + const verilog_identifier_exprt &item() const { - return static_cast(binary_exprt::op1()); + return static_cast(binary_exprt::op1()); } - const symbol_exprt &rhs() const + const verilog_identifier_exprt &rhs() const { return item(); } diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 83c81c150..39fed49a0 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -510,12 +510,12 @@ void verilog_synthesist::expand_hierarchical_identifier( const irep_idt &lhs_identifier = expr.lhs().get(ID_identifier); // rhs - const irep_idt &rhs_identifier = expr.rhs().get_identifier(); + const irep_idt &rhs_base_name = expr.rhs().base_name(); // just patch together irep_idt full_identifier = - id2string(lhs_identifier) + '.' + id2string(rhs_identifier); + id2string(lhs_identifier) + '.' + id2string(rhs_base_name); // Note: the instance copy may not yet be in symbol table, // as the inst module item may be later. diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 95d00513d..6e39a637e 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -962,7 +962,7 @@ void verilog_typecheckt::convert_parameter_override( auto module_instance = to_symbol_expr(hierarchical_identifier.module()).get_identifier(); - auto parameter_base_name = hierarchical_identifier.item().get_identifier(); + auto parameter_base_name = hierarchical_identifier.item().base_name(); // The rhs must be a constant at this point. auto rhs_value = diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index d1478b4c8..0ce66721a 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -1421,19 +1421,21 @@ exprt verilog_typecheck_exprt::convert_hierarchical_identifier( { convert_expr(expr.lhs()); - DATA_INVARIANT(expr.rhs().id() == ID_symbol, "expected symbol on rhs of `.'"); + DATA_INVARIANT( + expr.rhs().id() == ID_verilog_identifier, + "expected verilog_identifier as rhs of `.'"); - const irep_idt &rhs_identifier = expr.rhs().get_identifier(); + const irep_idt &rhs_base_name = expr.rhs().base_name(); if(expr.lhs().type().id() == ID_struct || expr.lhs().type().id() == ID_union) { // look up the component auto &compound_type = to_struct_union_type(expr.lhs().type()); - auto &component = compound_type.get_component(rhs_identifier); + auto &component = compound_type.get_component(rhs_base_name); if(component.is_nil()) throw errort().with_location(expr.source_location()) << compound_type.id() << " does not have a member named " - << rhs_identifier; + << rhs_base_name; // create the member expression return member_exprt{expr.lhs(), component.get_name(), component.type()} @@ -1467,7 +1469,7 @@ exprt verilog_typecheck_exprt::convert_hierarchical_identifier( // the identifier in the module const irep_idt full_identifier = - id2string(module) + "." + id2string(rhs_identifier); + id2string(module) + "." + id2string(rhs_base_name); const symbolt *symbol; if(!ns.lookup(full_identifier, symbol)) @@ -1485,7 +1487,7 @@ exprt verilog_typecheck_exprt::convert_hierarchical_identifier( else { throw errort().with_location(expr.source_location()) - << "identifier `" << rhs_identifier << "' not found in module `" + << "identifier `" << rhs_base_name << "' not found in module `" << module_instance_symbol->pretty_name << "'"; } @@ -1497,7 +1499,7 @@ exprt verilog_typecheck_exprt::convert_hierarchical_identifier( else if(expr.lhs().type().id() == ID_named_block) { const irep_idt full_identifier = - id2string(lhs_identifier) + "." + id2string(rhs_identifier); + id2string(lhs_identifier) + "." + id2string(rhs_base_name); const symbolt *symbol; if(!ns.lookup(full_identifier, symbol)) @@ -1519,7 +1521,7 @@ exprt verilog_typecheck_exprt::convert_hierarchical_identifier( else { throw errort().with_location(expr.source_location()) - << "identifier `" << rhs_identifier << "' not found in named block"; + << "identifier `" << rhs_base_name << "' not found in named block"; } } else