From 1dd80c45cac302af327d211abd6a7f40180516e8 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 21 Feb 2024 09:48:31 -0800 Subject: [PATCH] Verilog: enum constants may depend on elaboration-time constants This postpones the conversion of enum base types and enum initializers to enable them to depend on other elaboration-time constants. --- regression/verilog/enums/enum1.desc | 2 +- regression/verilog/enums/enum2.desc | 2 +- regression/verilog/enums/enum_base_type2.desc | 4 +-- .../verilog/enums/enum_initializers1.desc | 2 +- .../verilog/enums/enum_initializers2.desc | 7 ++--- .../verilog/enums/enum_initializers2.sv | 4 +-- .../verilog/enums/enum_initializers3.desc | 7 ++--- src/verilog/verilog_elaborate.cpp | 22 +++++++------- src/verilog/verilog_typecheck_expr.cpp | 27 +++++++++++++++-- src/verilog/verilog_typecheck_type.cpp | 5 ++++ src/verilog/verilog_types.h | 30 +++++++++++++++++++ 11 files changed, 81 insertions(+), 31 deletions(-) diff --git a/regression/verilog/enums/enum1.desc b/regression/verilog/enums/enum1.desc index aaf6323c0..8a1393455 100644 --- a/regression/verilog/enums/enum1.desc +++ b/regression/verilog/enums/enum1.desc @@ -3,5 +3,5 @@ enum1.sv --bound 3 ^EXIT=10$ ^SIGNAL=0$ -^\[main\.property\.p1\] always main\.my_light != 0 \+ 1 \+ 1 \+ 1: REFUTED$ +^\[main\.property\.p1\] always main\.my_light != 3: REFUTED$ -- diff --git a/regression/verilog/enums/enum2.desc b/regression/verilog/enums/enum2.desc index 096459417..b1d97f879 100644 --- a/regression/verilog/enums/enum2.desc +++ b/regression/verilog/enums/enum2.desc @@ -1,7 +1,7 @@ CORE enum2.sv -^file .* line 4: assignment to enum requires enum of the same type$ +^file .* line 4: assignment to enum requires enum of the same type, but got signed \[0:31\]$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/verilog/enums/enum_base_type2.desc b/regression/verilog/enums/enum_base_type2.desc index b71f85f40..bf0c25a09 100644 --- a/regression/verilog/enums/enum_base_type2.desc +++ b/regression/verilog/enums/enum_base_type2.desc @@ -1,9 +1,7 @@ -KNOWNBUG +CORE enum_base_type2.sv --bound 0 ^EXIT=0$ ^SIGNAL=0$ ^\[.*\] always 8 == 8: PROVED up to bound 0$ -- --- -The base type of an enum may depend on an elaboration-time constant. diff --git a/regression/verilog/enums/enum_initializers1.desc b/regression/verilog/enums/enum_initializers1.desc index 1d2fb66ac..b6f368f3c 100644 --- a/regression/verilog/enums/enum_initializers1.desc +++ b/regression/verilog/enums/enum_initializers1.desc @@ -2,7 +2,7 @@ CORE enum_initializers1.sv --bound 0 ^\[main\.property\.pA\] always 1 == 1: PROVED up to bound 0$ -^\[main\.property\.pB\] always 1 \+ 10 == 11: PROVED up to bound 0$ +^\[main\.property\.pB\] always 11 == 11: PROVED up to bound 0$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/enums/enum_initializers2.desc b/regression/verilog/enums/enum_initializers2.desc index 6b25722ba..d23baf2d7 100644 --- a/regression/verilog/enums/enum_initializers2.desc +++ b/regression/verilog/enums/enum_initializers2.desc @@ -1,9 +1,6 @@ -KNOWNBUG +CORE enum_initializers2.sv -^EXIT=10$ +^EXIT=0$ ^SIGNAL=0$ -- --- -Crashes with missing identifier - diff --git a/regression/verilog/enums/enum_initializers2.sv b/regression/verilog/enums/enum_initializers2.sv index 2c00dd618..fae70a7bd 100644 --- a/regression/verilog/enums/enum_initializers2.sv +++ b/regression/verilog/enums/enum_initializers2.sv @@ -2,11 +2,11 @@ module main; parameter B = A + 1; - enum { A = 1, C = my_parameter + 1 } my_enum; + enum { A = 1, C = B + 1 } my_enum; // expected to pass pA: assert property (A == 1); pB: assert property (B == 2); - pC: assert property (B == 3); + pC: assert property (C == 3); endmodule diff --git a/regression/verilog/enums/enum_initializers3.desc b/regression/verilog/enums/enum_initializers3.desc index b28e16d65..35d62ab73 100644 --- a/regression/verilog/enums/enum_initializers3.desc +++ b/regression/verilog/enums/enum_initializers3.desc @@ -1,8 +1,7 @@ -KNOWNBUG +CORE enum_initializers3.sv -^EXIT=10$ +^file .* line 4: cyclic dependency when elaborating main\.B$ +^EXIT=2$ ^SIGNAL=0$ -- --- -Cycle not detected. diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index 7e902876c..605f1a8ec 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -102,8 +102,9 @@ void verilog_typecheckt::collect_symbols(const typet &type) if(enum_type.has_base_type()) collect_symbols(enum_type.base_type()); - // convert the type now - auto converted_type = convert_type(enum_type); + // The type needs to be converted later, as it may + // depend on other elaboration-time constants. + auto tbd_type = to_be_elaborated_typet(enum_type); // Add the enum names to the symbol table for subsequent elaboration. // Values are given, or the previous plus one, starting with value '0'. @@ -111,28 +112,27 @@ void verilog_typecheckt::collect_symbols(const typet &type) for(auto &enum_name : enum_type.enum_names()) { + // The initializer will also be converted later. if(enum_name.value().is_not_nil()) - { - exprt tmp = enum_name.value(); - convert_expr(tmp); - initializer = std::move(tmp); - } + initializer = enum_name.value(); - exprt value = typecast_exprt(initializer, converted_type); + exprt value = typecast_exprt(initializer, tbd_type); + value.add_source_location() = enum_name.source_location(); const auto base_name = enum_name.base_name(); const auto identifier = hierarchical_identifier(base_name); - symbolt enum_name_symbol(identifier, converted_type, mode); + symbolt enum_name_symbol(identifier, tbd_type, mode); enum_name_symbol.module = module_identifier; enum_name_symbol.base_name = base_name; enum_name_symbol.value = std::move(value); enum_name_symbol.is_macro = true; enum_name_symbol.is_file_local = true; + enum_name_symbol.location = enum_name.source_location(); add_symbol(std::move(enum_name_symbol)); initializer = plus_exprt( - typecast_exprt(initializer, converted_type), - typecast_exprt(from_integer(1, integer_typet()), converted_type)); + typecast_exprt(initializer, tbd_type), + typecast_exprt(from_integer(1, integer_typet()), tbd_type)); } } } diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 4dcc3544f..a3a86185a 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -105,7 +105,8 @@ void verilog_typecheck_exprt::propagate_type( expr.type().get(ID_C_identifier) != type.get(ID_C_identifier)) { throw errort().with_location(expr.source_location()) - << "assignment to enum requires enum of the same type"; + << "assignment to enum requires enum of the same type, but got " + << to_string(expr.type()); } } @@ -1319,6 +1320,13 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression(exprt expr) } else { + // Remember the Verilog type. + auto expr_verilog_type = expr.type().get(ID_C_verilog_type); + auto expr_identifier = expr.type().get(ID_C_identifier); + + // Remember the source location. + auto location = expr.source_location(); + // Do any operands first. bool operands_are_constant = true; @@ -1344,7 +1352,19 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression(exprt expr) // We fall back to the simplifier to approximate // the standard's definition of 'constant expression'. - return simplify_expr(expr, ns); + auto simplified_expr = simplify_expr(expr, ns); + + // Restore the Verilog type, if any. + if(expr_verilog_type != irep_idt()) + simplified_expr.type().set(ID_C_verilog_type, expr_verilog_type); + + if(expr_identifier != irep_idt()) + simplified_expr.type().set(ID_C_identifier, expr_identifier); + + if(location.is_not_nil()) + simplified_expr.add_source_location() = location; + + return simplified_expr; } } @@ -1479,7 +1499,8 @@ void verilog_typecheck_exprt::implicit_typecast( expr.type().get(ID_C_identifier) != dest_type.get(ID_C_identifier)) { throw errort().with_location(expr.source_location()) - << "assignment to enum requires enum of the same type"; + << "assignment to enum requires enum of the same type, but got " + << to_string(expr.type()); } } diff --git a/src/verilog/verilog_typecheck_type.cpp b/src/verilog/verilog_typecheck_type.cpp index 840aba877..049511fa1 100644 --- a/src/verilog/verilog_typecheck_type.cpp +++ b/src/verilog/verilog_typecheck_type.cpp @@ -175,6 +175,11 @@ typet verilog_typecheck_exprt::convert_type(const typet &src) else return convert_type(type_reference.type_op()); } + else if(src.id() == ID_to_be_elaborated) + { + // recursive call + return convert_type(to_to_be_elaborated_type(src).subtype()); + } else { error().source_location = source_location; diff --git a/src/verilog/verilog_types.h b/src/verilog/verilog_types.h index 5f25065be..403b85e7b 100644 --- a/src/verilog/verilog_types.h +++ b/src/verilog/verilog_types.h @@ -22,6 +22,31 @@ class to_be_elaborated_typet : public type_with_subtypet } }; +/*! \brief Cast a generic typet to a \ref to_be_elaborated_typet + * + * This is an unchecked conversion. \a type must be known to be \ref + * to_be_elaborated_typet. + * + * \param type Source type + * \return Object of type \ref to_be_elaborated_typet + * + * \ingroup gr_std_types +*/ +inline const to_be_elaborated_typet &to_to_be_elaborated_type(const typet &type) +{ + PRECONDITION(type.id() == ID_to_be_elaborated); + return static_cast(type); +} + +/*! \copydoc to_to_be_elaborated_type(const typet &) + * \ingroup gr_std_types +*/ +inline to_be_elaborated_typet &to_to_be_elaborated_type(typet &type) +{ + PRECONDITION(type.id() == ID_to_be_elaborated); + return static_cast(type); +} + /// Used during elaboration only, /// to signal that the type of the symbol is going to be the /// type of the value (default for parameters). @@ -336,6 +361,11 @@ class verilog_enum_typet : public type_with_subtypet { set(ID_base_name, _base_name); } + + const source_locationt &source_location() const + { + return static_cast(find(ID_C_source_location)); + } }; using enum_namest = std::vector;