diff --git a/lib/cbmc b/lib/cbmc index fc4f7ca7..f2489e3e 160000 --- a/lib/cbmc +++ b/lib/cbmc @@ -1 +1 @@ -Subproject commit fc4f7ca71ddcbd290cea0d9ac58b6cc6f6b79cb0 +Subproject commit f2489e3edf77f95c5d43c4baf733607a073f8ccd diff --git a/regression/verilog/packages/package2.sv b/regression/verilog/packages/package2.sv index 39a465df..f0cebae8 100644 --- a/regression/verilog/packages/package2.sv +++ b/regression/verilog/packages/package2.sv @@ -6,8 +6,6 @@ endpackage module main; - import moo::*; - parameter Q = moo::P; assert final (Q == 123); diff --git a/regression/verilog/packages/package_typedef1.sv b/regression/verilog/packages/package_typedef1.sv index d43a9d11..4484e35d 100644 --- a/regression/verilog/packages/package_typedef1.sv +++ b/regression/verilog/packages/package_typedef1.sv @@ -6,8 +6,6 @@ endpackage module main; - import moo::*; - moo::my_type some_var; assert final ($typename(some_var) == "bit signed[7:0]"); diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp index f5ada047..b291782e 100644 --- a/src/verilog/verilog_elaborate_type.cpp +++ b/src/verilog/verilog_elaborate_type.cpp @@ -160,7 +160,7 @@ Function: verilog_typecheck_exprt::elaborate_package_scope_typedef \*******************************************************************/ typet verilog_typecheck_exprt::elaborate_package_scope_typedef( - const type_with_subtypest &src) + const verilog_package_scope_typet &src) { auto location = src.source_location(); @@ -445,7 +445,7 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src) else if(src.id() == ID_verilog_package_scope) { // package::typedef - return elaborate_package_scope_typedef(to_type_with_subtypes(src)); + return elaborate_package_scope_typedef(to_verilog_package_scope_type(src)); } else { diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp index 4358ca60..b42055f7 100644 --- a/src/verilog/verilog_expr.cpp +++ b/src/verilog/verilog_expr.cpp @@ -81,6 +81,34 @@ void verilog_module_sourcet::show(std::ostream &out) const out << '\n'; } +static void +dependencies_rec(const verilog_module_itemt &, std::vector &); + +static void dependencies_rec(const exprt &expr, std::vector &dest) +{ + if(expr.id() == ID_verilog_package_scope) + { + auto &package_scope_expr = to_verilog_package_scope_expr(expr); + dest.push_back( + verilog_package_identifier(package_scope_expr.package_base_name())); + } + else + { + for(auto &op : expr.operands()) + dependencies_rec(op, dest); + } +} + +static void dependencies_rec(const typet &type, std::vector &dest) +{ + if(type.id() == ID_verilog_package_scope) + { + auto &package_scope_type = to_verilog_package_scope_type(type); + dest.push_back( + verilog_package_identifier(package_scope_type.package_base_name())); + } +} + static void dependencies_rec( const verilog_module_itemt &module_item, std::vector &dest) @@ -114,6 +142,86 @@ static void dependencies_rec( verilog_package_identifier(import_item.get(ID_verilog_package))); } } + else if(module_item.id() == ID_parameter_decl) + { + auto ¶meter_decl = to_verilog_parameter_decl(module_item); + for(auto &decl : parameter_decl.declarations()) + { + dependencies_rec(decl.type(), dest); + dependencies_rec(decl.value(), dest); + } + } + else if(module_item.id() == ID_local_parameter_decl) + { + auto &localparam_decl = to_verilog_local_parameter_decl(module_item); + for(auto &decl : localparam_decl.declarations()) + { + dependencies_rec(decl.type(), dest); + dependencies_rec(decl.value(), dest); + } + } + else if(module_item.id() == ID_decl) + { + auto &decl = to_verilog_decl(module_item); + dependencies_rec(decl.type(), dest); + for(auto &declarator : decl.declarators()) + { + dependencies_rec(declarator.type(), dest); + dependencies_rec(declarator.value(), dest); + } + } + else if( + module_item.id() == ID_verilog_always || + module_item.id() == ID_verilog_always_comb || + module_item.id() == ID_verilog_always_ff || + module_item.id() == ID_verilog_always_latch) + { + dependencies_rec(to_verilog_always_base(module_item).statement(), dest); + } + else if(module_item.id() == ID_initial) + { + dependencies_rec(to_verilog_initial(module_item).statement(), dest); + } + else if(module_item.id() == ID_inst) + { + } + else if(module_item.id() == ID_inst_builtin) + { + } + else if(module_item.id() == ID_continuous_assign) + { + } + else if( + module_item.id() == ID_verilog_assert_property || + module_item.id() == ID_verilog_assume_property || + module_item.id() == ID_verilog_restrict_property || + module_item.id() == ID_verilog_cover_property) + { + } + else if(module_item.id() == ID_verilog_assertion_item) + { + } + else if(module_item.id() == ID_parameter_override) + { + } + else if(module_item.id() == ID_verilog_final) + { + } + else if(module_item.id() == ID_verilog_let) + { + // to_verilog_let(module_item)); + } + else if(module_item.id() == ID_verilog_smv_assume) + { + } + else if(module_item.id() == ID_verilog_property_declaration) + { + // to_verilog_property_declaration(module_item) + } + else if(module_item.id() == ID_verilog_sequence_declaration) + { + // to_verilog_sequence_declaration(module_item) + } } std::vector verilog_item_containert::dependencies() const diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index 4ee3d256..e97f8996 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -3011,4 +3011,39 @@ inline verilog_value_range_exprt &to_verilog_value_range_expr(exprt &expr) return static_cast(expr); } +/// package::identifier +class verilog_package_scope_exprt : public binary_exprt +{ +public: + irep_idt package_base_name() const + { + return op0().id(); + } + + const exprt &identifier() const + { + return op1(); + } +}; + +/// Cast a generic typet to a \ref verilog_package_scope_exprt. This is an unchecked +/// conversion. \a type must be known to be \ref verilog_package_scope_exprt. +/// \param type: Source type +/// \return Object of type \ref verilog_package_scope_exprt +inline const verilog_package_scope_exprt & +to_verilog_package_scope_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_verilog_package_scope); + verilog_package_scope_exprt::check(expr); + return static_cast(expr); +} + +/// \copydoc to_verilog_exprdef_expr(const exprt &) +inline verilog_package_scope_exprt &to_verilog_package_scope_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_verilog_package_scope); + verilog_package_scope_exprt::check(expr); + return static_cast(expr); +} + #endif diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 0f2a0fbd..d85f3c8d 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -2829,13 +2829,14 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) else if(expr.id() == ID_verilog_package_scope) { auto location = expr.source_location(); + auto &package_scope = to_verilog_package_scope_expr(expr); - if(expr.rhs().id() != ID_symbol) + if(package_scope.identifier().id() != ID_symbol) throw errort().with_location(location) << expr.id() << " expects symbol on the rhs"; - auto package_base = expr.lhs().id(); - auto rhs_base = expr.rhs().get(ID_base_name); + auto package_base = package_scope.package_base_name(); + auto rhs_base = package_scope.identifier().get(ID_base_name); // stitch together irep_idt full_identifier = diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h index eae33ead..b1aac8f9 100644 --- a/src/verilog/verilog_typecheck_expr.h +++ b/src/verilog/verilog_typecheck_expr.h @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com class function_call_exprt; class power_exprt; +class verilog_package_scope_typet; class verilog_typecheck_exprt:public verilog_typecheck_baset { @@ -66,7 +67,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 elaborate_package_scope_typedef(const verilog_package_scope_typet &); 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.cpp b/src/verilog/verilog_types.cpp index 9395b3a8..ed411efb 100644 --- a/src/verilog/verilog_types.cpp +++ b/src/verilog/verilog_types.cpp @@ -19,3 +19,15 @@ constant_exprt verilog_event_typet::null_expr() const { return encoding().all_zeros_expr(); } + +void verilog_package_scope_typet::check( + const typet &type, + const validation_modet vm) +{ + PRECONDITION(type.id() == ID_verilog_package_scope); + type_with_subtypest::check(type); + DATA_CHECK( + vm, + to_type_with_subtypes(type).subtypes().size() == 2, + "verilog_package_scope type must have two subtypes"); +} diff --git a/src/verilog/verilog_types.h b/src/verilog/verilog_types.h index 6149579b..81a95cf3 100644 --- a/src/verilog/verilog_types.h +++ b/src/verilog/verilog_types.h @@ -656,4 +656,42 @@ inline verilog_typedef_typet &to_verilog_typedef_type(typet &type) return static_cast(type); } +/// package::type +class verilog_package_scope_typet : public type_with_subtypest +{ +public: + irep_idt package_base_name() const + { + return subtypes()[0].id(); + } + + const typet &typedef_type() const + { + return subtypes()[1]; + } + + static void + check(const typet &, const validation_modet = validation_modet::INVARIANT); +}; + +/// Cast a generic typet to a \ref verilog_package_scope_typet. This is an unchecked +/// conversion. \a type must be known to be \ref verilog_package_scope_typet. +/// \param type: Source type +/// \return Object of type \ref verilog_package_scope_typet +inline const verilog_package_scope_typet & +to_verilog_package_scope_type(const typet &type) +{ + PRECONDITION(type.id() == ID_verilog_package_scope); + verilog_package_scope_typet::check(type); + return static_cast(type); +} + +/// \copydoc to_verilog_typedef_type(const typet &) +inline verilog_package_scope_typet &to_verilog_package_scope_type(typet &type) +{ + PRECONDITION(type.id() == ID_verilog_package_scope); + verilog_package_scope_typet::check(type); + return static_cast(type); +} + #endif