From 458793a39881efb61888e35369186f22428c8d01 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 29 Apr 2024 09:38:18 -0700 Subject: [PATCH 1/3] Verilog: use verilog_inst_baset::instancet This strenthens types in the Verilog front-end by using verilog_inst_baset::instancet instead of exprt. --- src/verilog/verilog_expr.h | 5 +++ src/verilog/verilog_typecheck.cpp | 53 +++++++++++++++++-------------- src/verilog/verilog_typecheck.h | 6 ++-- 3 files changed, 37 insertions(+), 27 deletions(-) diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index c53899d8c..6ae3170d2 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -596,6 +596,11 @@ class verilog_inst_baset : public verilog_module_itemt return operands(); } + exprt::operandst &connections() + { + return operands(); + } + protected: using exprt::operands; }; diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index bd0d920fe..ffb6cb3b2 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -78,7 +78,7 @@ Function: verilog_typecheckt::typecheck_port_connections \*******************************************************************/ void verilog_typecheckt::typecheck_port_connections( - exprt &inst, + verilog_inst_baset::instancet &inst, const symbolt &symbol) { const exprt &range=static_cast(inst.find(ID_range)); @@ -92,12 +92,15 @@ void verilog_typecheckt::typecheck_port_connections( const irept::subt &ports=symbol.type.find(ID_ports).get_sub(); - // no arguments is one argument that is nil - if(ports.size()==0 && inst.operands().size()==1 && - inst.operands().front().is_nil()) - inst.operands().clear(); + // no arguments is one argument that is nil + if( + ports.size() == 0 && inst.connections().size() == 1 && + inst.connections().front().is_nil()) + { + inst.connections().clear(); + } - if(inst.operands().empty()) + if(inst.connections().empty()) { if(!ports.empty()) { @@ -110,35 +113,37 @@ void verilog_typecheckt::typecheck_port_connections( // named port connection? - if(to_multi_ary_expr(inst).op0().id() == ID_named_port_connection) + if(inst.connections().front().id() == ID_named_port_connection) { // We don't require that all ports are connected. std::set assigned_ports; - Forall_operands(o_it, inst) + for(auto &connection : inst.connections()) { - if(o_it->id()!=ID_named_port_connection || - o_it->operands().size()!=2) + if( + connection.id() != ID_named_port_connection || + connection.operands().size() != 2) { throw errort().with_location(inst.source_location()) << "expected a named port connection"; } - exprt &op = to_binary_expr(*o_it).op1(); - const irep_idt &name = to_binary_expr(*o_it).op0().get(ID_identifier); + exprt &op = to_binary_expr(connection).op1(); + const irep_idt &name = + to_binary_expr(connection).op0().get(ID_identifier); bool found=false; std::string identifier= id2string(symbol.module)+"."+id2string(name); - to_binary_expr(*o_it).op0().set(ID_identifier, identifier); + to_binary_expr(connection).op0().set(ID_identifier, identifier); if(assigned_ports.find(name)!= assigned_ports.end()) { - throw errort().with_location(o_it->source_location()) + throw errort().with_location(connection.source_location()) << "port name " << name << " assigned twice"; } @@ -149,14 +154,14 @@ void verilog_typecheckt::typecheck_port_connections( auto &p_expr = static_cast(port); found=true; typecheck_port_connection(op, p_expr); - to_binary_expr(*o_it).op0().type() = p_expr.type(); + to_binary_expr(connection).op0().type() = p_expr.type(); break; } } if(!found) { - throw errort().with_location(o_it->source_location()) + throw errort().with_location(connection.source_location()) << "port name " << identifier << " not found"; } @@ -165,19 +170,19 @@ void verilog_typecheckt::typecheck_port_connections( } else // just a list without names { - if(inst.operands().size()!=ports.size()) + if(inst.connections().size() != ports.size()) { throw errort().with_location(inst.source_location()) << "wrong number of arguments: expected " << ports.size() << " but got " - << inst.operands().size(); + << inst.connections().size(); } irept::subt::const_iterator p_it= ports.begin(); - Forall_operands(o_it, inst) + for(auto &connection : inst.connections()) { - typecheck_port_connection(*o_it, (exprt &)*p_it); + typecheck_port_connection(connection, (exprt &)*p_it); p_it++; } } @@ -196,7 +201,7 @@ Function: verilog_typecheckt::typecheck_builtin_port_connections \*******************************************************************/ void verilog_typecheckt::typecheck_builtin_port_connections( - exprt &inst) + verilog_inst_baset::instancet &inst) { exprt &range=static_cast(inst.add(ID_range)); @@ -221,10 +226,10 @@ void verilog_typecheckt::typecheck_builtin_port_connections( type.set(ID_width, integer2string(width)); } - Forall_operands(o_it, inst) + for(auto &connection : inst.connections()) { - convert_expr(*o_it); - propagate_type(*o_it, type); + convert_expr(connection); + propagate_type(connection, type); } } diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h index 9bafda488..75c942308 100644 --- a/src/verilog/verilog_typecheck.h +++ b/src/verilog/verilog_typecheck.h @@ -177,15 +177,15 @@ class verilog_typecheckt: void instantiate_port_connections( const std::string &instance, - const exprt &inst, + const verilog_inst_baset::instancet &, const symbolt &symbol, exprt &trans); void typecheck_port_connections( - exprt &inst, + verilog_inst_baset::instancet &, const symbolt &symbol); - void typecheck_builtin_port_connections(exprt &inst); + void typecheck_builtin_port_connections(verilog_inst_baset::instancet &); void typecheck_port_connection( exprt &op, From 60e412b9fdc00d940ea3a37faa0578c13a68af8b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 29 Apr 2024 09:42:22 -0700 Subject: [PATCH 2/3] Verilog: KNOWNBUG test for inout port connected to variable An inout port must not be connected to a variable. --- regression/verilog/modules/inout_and_variable.desc | 9 +++++++++ regression/verilog/modules/inout_and_variable.v | 12 ++++++++++++ 2 files changed, 21 insertions(+) create mode 100644 regression/verilog/modules/inout_and_variable.desc create mode 100644 regression/verilog/modules/inout_and_variable.v diff --git a/regression/verilog/modules/inout_and_variable.desc b/regression/verilog/modules/inout_and_variable.desc new file mode 100644 index 000000000..6143de355 --- /dev/null +++ b/regression/verilog/modules/inout_and_variable.desc @@ -0,0 +1,9 @@ +KNOWNBUG +inout_and_variable.v + +^file .* line 4: symbol `some_var' is declared both as input and as register$ +^EXIT=2$ +^SIGNAL=0$ +-- +-- +The use of a variable with an inout port should be rejected. diff --git a/regression/verilog/modules/inout_and_variable.v b/regression/verilog/modules/inout_and_variable.v new file mode 100644 index 000000000..e8f9a3a92 --- /dev/null +++ b/regression/verilog/modules/inout_and_variable.v @@ -0,0 +1,12 @@ +module sub(inout some_port); + +endmodule + +module main; + // 1800-2017 6.5 + // "Variables cannot be connected to either side of an inout port" + reg my_var; + + sub sub(my_var); + +endmodule From 086256a703ce64ff5f778077ae833dc3c8f1425d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 29 Apr 2024 09:51:56 -0700 Subject: [PATCH 3/3] introduce verilog_inst_baset::named_port_connectiont This class documents an existing expression type in the Verilog frontend. --- src/verilog/verilog_expr.h | 49 +++++++++++++++++++++++++++++++ src/verilog/verilog_typecheck.cpp | 18 ++++++------ 2 files changed, 58 insertions(+), 9 deletions(-) diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index 6ae3170d2..95e1a4510 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -573,6 +573,39 @@ class verilog_inst_baset : public verilog_module_itemt return set(ID_module, module); } + class named_port_connectiont : public binary_exprt + { + public: + named_port_connectiont(exprt _port, exprt _value) + : binary_exprt( + std::move(_port), + ID_named_port_connection, + std::move(_value), + typet{}) + { + } + + const exprt &port() const + { + return op0(); + } + + exprt &port() + { + return op0(); + } + + const exprt &value() const + { + return op1(); + } + + exprt &value() + { + return op1(); + } + }; + class instancet : public exprt { public: @@ -621,6 +654,22 @@ class verilog_inst_baset : public verilog_module_itemt using exprt::operands; }; +inline const verilog_inst_baset::named_port_connectiont & +to_verilog_named_port_connection(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_named_port_connection); + verilog_inst_baset::named_port_connectiont::check(expr); + return static_cast(expr); +} + +inline verilog_inst_baset::named_port_connectiont & +to_verilog_named_port_connection(exprt &expr) +{ + PRECONDITION(expr.id() == ID_named_port_connection); + verilog_inst_baset::named_port_connectiont::check(expr); + return static_cast(expr); +} + class verilog_instt : public verilog_inst_baset { public: diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index ffb6cb3b2..d9b6f62ae 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -121,24 +121,24 @@ void verilog_typecheckt::typecheck_port_connections( for(auto &connection : inst.connections()) { - if( - connection.id() != ID_named_port_connection || - connection.operands().size() != 2) + if(connection.id() != ID_named_port_connection) { throw errort().with_location(inst.source_location()) << "expected a named port connection"; } - exprt &op = to_binary_expr(connection).op1(); - const irep_idt &name = - to_binary_expr(connection).op0().get(ID_identifier); + auto &named_port_connection = + to_verilog_named_port_connection(connection); + + exprt &value = named_port_connection.value(); + const irep_idt &name = named_port_connection.port().get(ID_identifier); bool found=false; std::string identifier= id2string(symbol.module)+"."+id2string(name); - to_binary_expr(connection).op0().set(ID_identifier, identifier); + named_port_connection.port().set(ID_identifier, identifier); if(assigned_ports.find(name)!= assigned_ports.end()) @@ -153,8 +153,8 @@ void verilog_typecheckt::typecheck_port_connections( { auto &p_expr = static_cast(port); found=true; - typecheck_port_connection(op, p_expr); - to_binary_expr(connection).op0().type() = p_expr.type(); + typecheck_port_connection(value, p_expr); + named_port_connection.port().type() = p_expr.type(); break; } }