diff --git a/lib/cbmc b/lib/cbmc index a8b8f0fd2..2ffc4c911 160000 --- a/lib/cbmc +++ b/lib/cbmc @@ -1 +1 @@ -Subproject commit a8b8f0fd2ad2166d71ccce97dd6925198a018144 +Subproject commit 2ffc4c911f4181fa66bb98bdd32d8dd517e5d8b2 diff --git a/regression/verilog/unions/unions1.desc b/regression/verilog/unions/unions1.desc new file mode 100644 index 000000000..5061ce31e --- /dev/null +++ b/regression/verilog/unions/unions1.desc @@ -0,0 +1,8 @@ +KNOWNBUG +unions1.sv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +-- +cast bitvector to union missing diff --git a/regression/verilog/unions/unions1.sv b/regression/verilog/unions/unions1.sv new file mode 100644 index 000000000..d24e50791 --- /dev/null +++ b/regression/verilog/unions/unions1.sv @@ -0,0 +1,16 @@ +module main; + + union packed { + bit [6:0] field1; + bit [6:0] field2; + } u; + + // bit-vectors can be converted without cast to packed unions + initial u = 7'b1010101; + + // Expected to pass. + p0: assert property ($bits(u) == 7); + p1: assert property (u.field1 == 7'b1010101); + p2: assert property (u.field2 == 7'b1010101); + +endmodule diff --git a/regression/verilog/unions/unions2.desc b/regression/verilog/unions/unions2.desc new file mode 100644 index 000000000..c483905b0 --- /dev/null +++ b/regression/verilog/unions/unions2.desc @@ -0,0 +1,7 @@ +CORE +unions2.sv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/regression/verilog/unions/unions2.sv b/regression/verilog/unions/unions2.sv new file mode 100644 index 000000000..2007c4b51 --- /dev/null +++ b/regression/verilog/unions/unions2.sv @@ -0,0 +1,18 @@ +module main; + + union { + bit field1; + bit [6:0] field2; + } u; + + initial begin + u.field2 = 0; + u.field1 = 1; + end + + // Expected to pass. + p1: assert property (u.field1 == 1); + p2: assert property (u.field2 == 1); + p3: assert property ($bits(u) == 7); + +endmodule diff --git a/regression/verilog/unions/unions3.desc b/regression/verilog/unions/unions3.desc new file mode 100644 index 000000000..7af55b1d4 --- /dev/null +++ b/regression/verilog/unions/unions3.desc @@ -0,0 +1,7 @@ +CORE +unions3.sv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/regression/verilog/unions/unions3.sv b/regression/verilog/unions/unions3.sv new file mode 100644 index 000000000..e79a87348 --- /dev/null +++ b/regression/verilog/unions/unions3.sv @@ -0,0 +1,19 @@ +module main; + + union packed { + // a struct inside a union + struct packed { + bit [7:0] field1; + } field1; + + bit [7:0] field2; + } u; + + initial begin + u.field1.field1 = 123; + end + + // Expected to pass. + p1: assert property (u.field2 == 123); + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 8a03fda97..2eaa508ee 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -149,6 +149,7 @@ IREP_ID_ONE(wand) IREP_ID_ONE(automatic) IREP_ID_TWO(C_verilog_type, #verilog_type) IREP_ID_ONE(verilog_enum) +IREP_ID_ONE(verilog_packed) IREP_ID_ONE(verilog_packed_array) IREP_ID_ONE(verilog_type_reference) IREP_ID_ONE(verilog_unpacked_array) diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index d02c0c737..f3c7deacd 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -831,7 +831,9 @@ void verilog_synthesist::assignment_rec( const exprt &lhs_compound = member_expr.struct_op(); auto component_name = member_expr.get_component_name(); - if(lhs_compound.type().id() == ID_struct) + if( + lhs_compound.type().id() == ID_struct || + lhs_compound.type().id() == ID_union) { // turn // s.m=e diff --git a/src/verilog/verilog_typecheck_base.cpp b/src/verilog/verilog_typecheck_base.cpp index 6287f4665..ddc461383 100644 --- a/src/verilog/verilog_typecheck_base.cpp +++ b/src/verilog/verilog_typecheck_base.cpp @@ -6,7 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include +#include "verilog_typecheck_base.h" #include #include @@ -14,7 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "expr2verilog.h" -#include "verilog_typecheck_base.h" +#include "verilog_types.h" + +#include /*******************************************************************\ @@ -157,7 +159,7 @@ mp_integer verilog_typecheck_baset::array_offset(const array_typet &type) /*******************************************************************\ -Function: verilog_typecheck_baset::get_width +Function: verilog_typecheck_baset::get_width_opt Inputs: @@ -167,7 +169,8 @@ Function: verilog_typecheck_baset::get_width \*******************************************************************/ -mp_integer verilog_typecheck_baset::get_width(const typet &type) +std::optional +verilog_typecheck_baset::get_width_opt(const typet &type) { if(type.id()==ID_bool) return 1; @@ -178,8 +181,11 @@ mp_integer verilog_typecheck_baset::get_width(const typet &type) if(type.id()==ID_array) { - mp_integer element_width = get_width(to_array_type(type).element_type()); - return (array_size(to_array_type(type)) * element_width).to_ulong(); + auto element_width = get_width_opt(to_array_type(type).element_type()); + if(element_width.has_value()) + return array_size(to_array_type(type)) * element_width.value(); + else + return {}; } if(type.id() == ID_struct) @@ -187,10 +193,24 @@ mp_integer verilog_typecheck_baset::get_width(const typet &type) // add them up mp_integer sum = 0; for(auto &component : to_struct_type(type).components()) - sum += get_width(component.type()); + { + auto component_width = get_width_opt(component.type()); + if(!component_width.has_value()) + return {}; + sum += *component_width; + } return sum; } + if(type.id() == ID_union) + { + // find the biggest + mp_integer max = 0; + for(auto &component : to_verilog_union_type(type).components()) + max = std::max(max, get_width(component.type())); + return max; + } + if(type.id() == ID_verilog_shortint) return 16; else if(type.id() == ID_verilog_int) @@ -202,8 +222,30 @@ mp_integer verilog_typecheck_baset::get_width(const typet &type) else if(type.id() == ID_verilog_time) return 64; - throw errort().with_location(type.source_location()) - << "type `" << type.id() << "' has unknown width"; + return {}; +} + +/*******************************************************************\ + +Function: verilog_typecheck_baset::get_width + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +mp_integer verilog_typecheck_baset::get_width(const typet &type) +{ + auto width_opt = get_width_opt(type); + + if(width_opt.has_value()) + return std::move(width_opt.value()); + else + throw errort().with_location(type.source_location()) + << "type `" << type.id() << "' has unknown width"; } /*******************************************************************\ diff --git a/src/verilog/verilog_typecheck_base.h b/src/verilog/verilog_typecheck_base.h index 7a6c7bda1..074b9f698 100644 --- a/src/verilog/verilog_typecheck_base.h +++ b/src/verilog/verilog_typecheck_base.h @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_VERILOG_TYPECHEK_BASE_H #define CPROVER_VERILOG_TYPECHEK_BASE_H +#include #include #include #include @@ -44,14 +45,16 @@ class verilog_typecheck_baset:public typecheckt const namespacet &ns; const irep_idt mode; - mp_integer get_width(const exprt &expr) + static mp_integer get_width(const exprt &expr) { return get_width(expr.type()); } - mp_integer get_width(const typet &type); - mp_integer array_size(const array_typet &); - mp_integer array_offset(const array_typet &); - typet index_type(const array_typet &); + + static mp_integer get_width(const typet &); + static std::optional get_width_opt(const typet &); + static mp_integer array_size(const array_typet &); + static mp_integer array_offset(const array_typet &); + static typet index_type(const array_typet &); }; #endif diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 62aa6cff9..4917c976b 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -434,7 +434,7 @@ Function: verilog_typecheck_exprt::bits exprt verilog_typecheck_exprt::bits(const exprt &expr) { - auto width_opt = bits_rec(expr.type()); + auto width_opt = get_width_opt(expr.type()); if(!width_opt.has_value()) { @@ -447,57 +447,6 @@ exprt verilog_typecheck_exprt::bits(const exprt &expr) /*******************************************************************\ -Function: verilog_typecheck_exprt::bits_rec - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -std::optional -verilog_typecheck_exprt::bits_rec(const typet &type) const -{ - if(type.id() == ID_bool) - return 1; - else if(type.id() == ID_unsignedbv) - return to_unsignedbv_type(type).get_width(); - else if(type.id() == ID_signedbv) - return to_signedbv_type(type).get_width(); - else if(type.id() == ID_integer) - return 32; - else if(type.id() == ID_array) - { - auto &array_type = to_array_type(type); - auto size_int = - numeric_cast_v(to_constant_expr(array_type.size())); - auto element_bits_opt = bits_rec(array_type.element_type()); - if(element_bits_opt.has_value()) - return element_bits_opt.value() * size_int; - else - return {}; - } - else if(type.id() == ID_struct) - { - auto &struct_type = to_struct_type(type); - mp_integer sum = 0; - for(auto &component : struct_type.components()) - { - auto component_bits_opt = bits_rec(component.type()); - if(!component_bits_opt.has_value()) - return component_bits_opt.value(); - sum += component_bits_opt.value(); - } - return sum; - } - else - return {}; -} - -/*******************************************************************\ - Function: verilog_typecheck_exprt::convert_system_function Inputs: @@ -1644,16 +1593,17 @@ void verilog_typecheck_exprt::implicit_typecast( expr = typecast_exprt{expr, dest_type}; return; } - else if(dest_type.id() == ID_struct) + else if(dest_type.id() == ID_struct || dest_type.id() == ID_union) { - // bit-vectors can be converted to packed structs + // bit-vectors can be converted to + // packed structs and packed unions expr = typecast_exprt{expr, dest_type}; return; } } - else if(src_type.id() == ID_struct) + else if(src_type.id() == ID_struct || src_type.id() == ID_union) { - // packed structs can be converted to bits + // packed structs and packed unions can be converted to bits if( dest_type.id() == ID_bool || dest_type.id() == ID_unsignedbv || dest_type.id() == ID_signedbv || diff --git a/src/verilog/verilog_types.h b/src/verilog/verilog_types.h index 2f05e17c2..73db4c5ce 100644 --- a/src/verilog/verilog_types.h +++ b/src/verilog/verilog_types.h @@ -484,4 +484,59 @@ inline verilog_type_referencet &to_verilog_type_reference(typet &type) return static_cast(type); } +/// The SystemVerilog struct/union type +class verilog_struct_union_typet : public struct_union_typet +{ +public: + verilog_struct_union_typet( + irep_idt __id, + bool __is_packed, + componentst _components) + : struct_union_typet(__id, std::move(_components)) + { + is_packed(__is_packed); + } + + bool is_packed() const + { + return get_bool(ID_verilog_packed); + } + + void is_packed(bool __is_packed) + { + return set(ID_verilog_packed, __is_packed); + } +}; + +/// The SystemVerilog union type +class verilog_union_typet : public verilog_struct_union_typet +{ +public: + verilog_union_typet(bool __is_packed, componentst _components) + : verilog_struct_union_typet(ID_union, __is_packed, std::move(_components)) + { + } +}; + +/// \brief Cast a typet to a \ref verilog_union_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// verilog_union_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref verilog_union_typet +inline const verilog_union_typet &to_verilog_union_type(const typet &type) +{ + PRECONDITION(type.id() == ID_union); + return static_cast(type); +} + +/// \copydoc to_union_type(const typet &) +inline verilog_union_typet &to_verilog_union_type(typet &type) +{ + PRECONDITION(type.id() == ID_union); + return static_cast(type); +} + #endif