From 7b190e01c2074e162b110719b5fafcbd1a72473c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 17 Oct 2025 15:51:53 -0700 Subject: [PATCH 1/2] Verilog: fixup for #1318 This deletes the assignment conversion code from verilog_typecheck.cpp, which was omitted from #1318. --- src/verilog/verilog_typecheck.cpp | 213 ------------------------------ src/verilog/verilog_typecheck.h | 2 - 2 files changed, 215 deletions(-) diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 0f805edf0..0c9a845d5 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -27,219 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ -Function: verilog_typecheckt::assignment_conversion - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void verilog_typecheckt::assignment_conversion( - exprt &rhs, - const typet &lhs_type) -{ - // 1800-2017 10.9 - if(rhs.type().id() == ID_verilog_assignment_pattern) - { - DATA_INVARIANT( - rhs.id() == ID_verilog_assignment_pattern, - "verilog_assignment_pattern expression expected"); - - if(lhs_type.id() == ID_struct) - { - auto &struct_type = to_struct_type(lhs_type); - auto &components = struct_type.components(); - - if( - !rhs.operands().empty() && - rhs.operands().front().id() == ID_member_initializer) - { - exprt::operandst initializers{components.size(), nil_exprt{}}; - - for(auto &op : rhs.operands()) - { - PRECONDITION(op.id() == ID_member_initializer); - auto member_name = op.get(ID_member_name); - if(!struct_type.has_component(member_name)) - { - throw errort().with_location(op.source_location()) - << "struct does not have a member `" << member_name << "'"; - } - auto nr = struct_type.component_number(member_name); - auto value = to_unary_expr(op).op(); - // rec. call - assignment_conversion(value, components[nr].type()); - initializers[nr] = std::move(value); - } - - // Is every member covered? - for(std::size_t i = 0; i < components.size(); i++) - if(initializers[i].is_nil()) - { - throw errort().with_location(rhs.source_location()) - << "assignment pattern does not assign member `" - << components[i].get_name() << "'"; - } - - rhs = struct_exprt{std::move(initializers), struct_type} - .with_source_location(rhs.source_location()); - } - else - { - if(rhs.operands().size() != components.size()) - { - throw errort().with_location(rhs.source_location()) - << "number of expressions does not match number of struct members"; - } - - for(std::size_t i = 0; i < components.size(); i++) - { - // rec. call - assignment_conversion(rhs.operands()[i], components[i].type()); - } - - // turn into struct expression - rhs.id(ID_struct); - rhs.type() = lhs_type; - } - - return; - } - else if(lhs_type.id() == ID_array) - { - auto &array_type = to_array_type(lhs_type); - auto &element_type = array_type.element_type(); - auto array_size = - numeric_cast_v(to_constant_expr(array_type.size())); - - if(array_size != rhs.operands().size()) - { - throw errort().with_location(rhs.source_location()) - << "number of expressions does not match number of array elements"; - } - - for(std::size_t i = 0; i < array_size; i++) - { - // rec. call - assignment_conversion(rhs.operands()[i], element_type); - } - - // turn into array expression - rhs.id(ID_array); - rhs.type() = lhs_type; - return; - } - else - { - throw errort().with_location(rhs.source_location()) - << "cannot convert assignment pattern to '" << to_string(lhs_type) - << '\''; - } - } - - auto original_rhs_type = rhs.type(); // copy - - auto &verilog_dest_type = lhs_type.get(ID_C_verilog_type); - if(verilog_dest_type == ID_verilog_enum) - { - // IEEE 1800-2017 6.19.3: "a variable of type enum cannot be directly - // assigned a value that lies outside the enumeration set unless an - // explicit cast is used" - if( - rhs.type().get(ID_C_verilog_type) != ID_verilog_enum || - rhs.type().get(ID_C_identifier) != lhs_type.get(ID_C_identifier)) - { - throw errort().with_location(rhs.source_location()) - << "assignment to enum requires enum of the same type, but got " - << to_string(rhs.type()); - } - } - - if(lhs_type == rhs.type()) - return; - - // do enum, union and struct decay - enum_decay(rhs); - struct_decay(rhs); - union_decay(rhs); - - if(rhs.type().id() == ID_struct || rhs.type().id() == ID_union) - { - // not decayed, not equal - throw errort().with_location(rhs.source_location()) - << "failed to convert `" << to_string(original_rhs_type) << "' to `" - << to_string(lhs_type) << "'"; - } - - // Implements 1800-2017 10.7 and 1800-2017 11.8.3. - - if( - lhs_type.id() == ID_verilog_real || lhs_type.id() == ID_verilog_shortreal || - lhs_type.id() == ID_verilog_realtime || - rhs.type().id() == ID_verilog_real || - rhs.type().id() == ID_verilog_shortreal) - { - // from/to real is just a cast - rhs = typecast_exprt::conditional_cast(rhs, lhs_type); - return; - } - - if(rhs.type().id() == ID_verilog_null) - { - if( - lhs_type.id() == ID_verilog_chandle || - lhs_type.id() == ID_verilog_class_type || - lhs_type.id() == ID_verilog_event) - { - rhs = typecast_exprt{rhs, lhs_type}; - return; - } - } - - // "The size of the left-hand side of an assignment forms - // the context for the right-hand expression." - - // Get the width of LHS and RHS - auto lhs_width = get_width(lhs_type); - auto rhs_width = get_width(rhs.type()); - - if(lhs_width > rhs_width) - { - // Need to enlarge the RHS. - // - // "If needed, extend the size of the right-hand side, - // performing sign extension if, and only if, the type - // of the right-hand side is signed. - if( - (rhs.type().id() == ID_signedbv || - rhs.type().id() == ID_verilog_signedbv) && - (lhs_type.id() == ID_unsignedbv || - lhs_type.id() == ID_verilog_unsignedbv)) - { - // LHS is unsigned, RHS is signed. Must sign-extend. - auto new_rhs_type = to_bitvector_type(rhs.type()); - new_rhs_type.set_width(numeric_cast_v(lhs_width)); - - downwards_type_propagation(rhs, new_rhs_type); - - // then cast - rhs = typecast_exprt::conditional_cast(rhs, lhs_type); - } - else - downwards_type_propagation(rhs, lhs_type); - } - else - { - // no need to enlarge - rhs = typecast_exprt::conditional_cast(rhs, lhs_type); - } -} - -/*******************************************************************\ - Function: verilog_typecheckt::typecheck_port_connection Inputs: diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h index ffa6cd276..4d0ce747b 100644 --- a/src/verilog/verilog_typecheck.h +++ b/src/verilog/verilog_typecheck.h @@ -168,8 +168,6 @@ class verilog_typecheckt: void convert_assert_assume_cover(verilog_assert_assume_cover_statementt &); void convert_assume(verilog_assume_statementt &); - void assignment_conversion(exprt &rhs, const typet &lhs_type); - // module items void convert_decl(class verilog_declt &); void convert_function_or_task(class verilog_function_or_task_declt &); From 328ca3d1ba115ca58e290270762fc8f98bd22a90 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 17 Oct 2025 15:55:01 -0700 Subject: [PATCH 2/2] Verilog: refuse assignments of other types to unpacked structs This errors assignments of any other type to an unpacked struct. --- regression/verilog/structs/unpacked_struct2.desc | 7 +++++++ regression/verilog/structs/unpacked_struct2.sv | 11 +++++++++++ src/verilog/verilog_typecheck_expr.cpp | 8 ++++++++ 3 files changed, 26 insertions(+) create mode 100644 regression/verilog/structs/unpacked_struct2.desc create mode 100644 regression/verilog/structs/unpacked_struct2.sv diff --git a/regression/verilog/structs/unpacked_struct2.desc b/regression/verilog/structs/unpacked_struct2.desc new file mode 100644 index 000000000..f1c99907d --- /dev/null +++ b/regression/verilog/structs/unpacked_struct2.desc @@ -0,0 +1,7 @@ +CORE +unpacked_struct2.sv + +^file .* line 9: failed to convert `signed \[31:0\]' to `struct'$ +^EXIT=2$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/structs/unpacked_struct2.sv b/regression/verilog/structs/unpacked_struct2.sv new file mode 100644 index 000000000..e267aa30f --- /dev/null +++ b/regression/verilog/structs/unpacked_struct2.sv @@ -0,0 +1,11 @@ +module main; + + // an unpacked struct type + typedef struct { + bit field; + } s_type; + + // bit-vectors cannot be assigned to unpacked structs + wire s_type w = 123; + +endmodule diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 08fa98eab..02f8bd7e0 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -223,6 +223,14 @@ void verilog_typecheck_exprt::assignment_conversion( if(lhs_type == rhs.type()) return; + if(lhs_type.id() == ID_struct && !lhs_type.get_bool(ID_packed)) + { + // assignment of a non-matching type to unpacked struct + throw errort().with_location(rhs.source_location()) + << "failed to convert `" << to_string(original_rhs_type) << "' to `" + << to_string(lhs_type) << "'"; + } + // do enum, union and struct decay enum_decay(rhs); struct_decay(rhs);