diff --git a/regression/verilog/functioncall/functioncall_as_constant1.desc b/regression/verilog/functioncall/functioncall_as_constant1.desc index a9b05c22d..85083a7dd 100644 --- a/regression/verilog/functioncall/functioncall_as_constant1.desc +++ b/regression/verilog/functioncall/functioncall_as_constant1.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE functioncall_as_constant1.v --module main --bound 0 ^EXIT=0$ diff --git a/regression/verilog/functioncall/functioncall_as_constant1.v b/regression/verilog/functioncall/functioncall_as_constant1.v index 8d475b09a..884a50900 100644 --- a/regression/verilog/functioncall/functioncall_as_constant1.v +++ b/regression/verilog/functioncall/functioncall_as_constant1.v @@ -1,6 +1,7 @@ module main; - function [31:0] clog2(input [63:0] value); + function [31:0] clog2; + input [63:0] value; reg [63:0] tmp; begin tmp = value - 1; diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index cfef3e3e1..74dd5adba 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -169,89 +169,170 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl) decl_class == ID_input || decl_class == ID_output || decl_class == ID_output_register || decl_class == ID_inout) { - // function ports are done in interface_function_or_task - if(!function_or_task_name.empty()) - return; + // If these are inputs/outputs of a function/task, then + // adjust the function/task signature. + if(function_or_task_name.empty()) + { + symbolt symbol; - symbolt symbol; + symbol.mode = mode; + symbol.module = module_identifier; + symbol.value.make_nil(); - symbol.mode = mode; - symbol.module = module_identifier; - symbol.value.make_nil(); + auto type = convert_type(decl.type()); - auto type = convert_type(decl.type()); + if(decl_class == ID_input) + symbol.is_input = true; + else if(decl_class == ID_output) + symbol.is_output = true; + else if(decl_class == ID_output_register) + { + symbol.is_output = true; + symbol.is_state_var = true; + } + else if(decl_class == ID_inout) + { + symbol.is_input = true; + symbol.is_output = true; + } - if(decl_class == ID_input) - symbol.is_input = true; - else if(decl_class == ID_output) - symbol.is_output = true; - else if(decl_class == ID_output_register) - { - symbol.is_output = true; - symbol.is_state_var = true; + for(auto &declarator : decl.declarators()) + { + DATA_INVARIANT( + declarator.id() == ID_declarator, "must have declarator"); + + symbol.base_name = declarator.base_name(); + symbol.location = declarator.source_location(); + + if(declarator.type().is_nil()) + symbol.type = type; + else if(declarator.type().id() == ID_array) + symbol.type = array_type(declarator.type(), type); + else + { + throw errort().with_location(declarator.source_location()) + << "unexpected type on declarator"; + } + + if(symbol.base_name.empty()) + { + throw errort().with_location(decl.source_location()) + << "empty symbol name"; + } + + symbol.name = hierarchical_identifier(symbol.base_name); + symbol.pretty_name = strip_verilog_prefix(symbol.name); + + auto result = symbol_table.get_writeable(symbol.name); + + if(result == nullptr) + { + symbol_table.add(symbol); + } + else + { + symbolt &osymbol = *result; + + if(symbol.type != osymbol.type) + { + if(get_width(symbol.type) > get_width(osymbol.type)) + osymbol.type = symbol.type; + } + + osymbol.is_input = symbol.is_input || osymbol.is_input; + osymbol.is_output = symbol.is_output || osymbol.is_output; + osymbol.is_state_var = symbol.is_state_var || osymbol.is_state_var; + + // a register can't be an input as well + if(osymbol.is_input && osymbol.is_state_var) + { + throw errort().with_location(declarator.source_location()) + << "port `" << symbol.base_name + << "' is declared both as input and as register"; + } + } + + symbols_added.push_back(symbol.name); + } } - else if(decl_class == ID_inout) + else { - symbol.is_input = true; - symbol.is_output = true; - } + symbolt symbol; + bool input = false, output = false; - for(auto &declarator : decl.declarators()) - { - DATA_INVARIANT(declarator.id() == ID_declarator, "must have declarator"); + symbol.mode = mode; + symbol.module = module_identifier; + symbol.value.make_nil(); - symbol.base_name = declarator.base_name(); - symbol.location = declarator.source_location(); + auto type = convert_type(decl.type()); - if(declarator.type().is_nil()) - symbol.type = type; - else if(declarator.type().id() == ID_array) - symbol.type = array_type(declarator.type(), type); - else + symbol.is_state_var = true; + + if(decl_class == ID_input) { - throw errort().with_location(declarator.source_location()) - << "unexpected type on declarator"; + input = true; } - - if(symbol.base_name.empty()) + else if(decl_class == ID_output) { - throw errort().with_location(decl.source_location()) - << "empty symbol name"; + output = true; } - - symbol.name = hierarchical_identifier(symbol.base_name); - symbol.pretty_name = strip_verilog_prefix(symbol.name); - - auto result = symbol_table.get_writeable(symbol.name); - - if(result == nullptr) + else if(decl_class == ID_output_register) { - symbol_table.add(symbol); + output = true; } - else + else if(decl_class == ID_inout) { - symbolt &osymbol = *result; + input = true; + output = true; + } - if(symbol.type != osymbol.type) + for(auto &declarator : decl.declarators()) + { + DATA_INVARIANT( + declarator.id() == ID_declarator, "must have declarator"); + + symbol.base_name = declarator.base_name(); + + if(symbol.base_name.empty()) { - if(get_width(symbol.type) > get_width(osymbol.type)) - osymbol.type = symbol.type; + throw errort().with_location(decl.source_location()) + << "empty symbol name"; } - osymbol.is_input = symbol.is_input || osymbol.is_input; - osymbol.is_output = symbol.is_output || osymbol.is_output; - osymbol.is_state_var = symbol.is_state_var || osymbol.is_state_var; + symbol.type = type; - // a register can't be an input as well - if(osymbol.is_input && osymbol.is_state_var) + symbol.name = hierarchical_identifier(symbol.base_name); + + symbol.pretty_name = strip_verilog_prefix(symbol.name); + + if(input || output) { - throw errort().with_location(declarator.source_location()) - << "port `" << symbol.base_name - << "' is declared both as input and as register"; + // Terminology clash: these aren't called 'parameters' + // in Verilog terminology, but inputs and outputs. + // We'll use the C terminology, and call them parameters. + // Not to be confused with module parameters. + symbolt &function_or_task_symbol = + symbol_table.get_writeable_ref(function_or_task_name); + code_typet::parameterst ¶meters = + to_code_type(function_or_task_symbol.type).parameters(); + parameters.push_back(code_typet::parametert(symbol.type)); + code_typet::parametert ¶meter = parameters.back(); + parameter.set_base_name(symbol.base_name); + parameter.set_identifier(symbol.name); + parameter.set(ID_output, output); + parameter.set(ID_input, input); } - } - symbols_added.push_back(symbol.name); + auto result = symbol_table.symbols.find(symbol.name); + + if(result != symbol_table.symbols.end()) + { + throw errort().with_location(decl.source_location()) + << "symbol `" << symbol.base_name << "' is already declared"; + } + + symbol_table.add(symbol); + } } } else if(decl_class == ID_verilog_genvar) @@ -365,6 +446,54 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl) } else if(decl_class == ID_function || decl_class == ID_task) { + typet return_type; + + if(decl_class == ID_function) + return_type = convert_type(decl.type()); + else + return_type = empty_typet(); + + auto base_name = decl.get_identifier(); + auto identifier = hierarchical_identifier(base_name); + symbolt symbol{identifier, code_typet{{}, std::move(return_type)}, mode}; + + symbol.base_name = base_name; + symbol.pretty_name = strip_verilog_prefix(symbol.name); + symbol.module = module_identifier; + symbol.value = decl; + + add_symbol(symbol); + + function_or_task_name = symbol.name; + + // add a symbol for the return value of functions, if applicable + + if(decl_class == ID_function) + { + symbolt return_symbol; + return_symbol.is_state_var = true; + return_symbol.is_lvalue = true; + return_symbol.mode = symbol.mode; + return_symbol.module = symbol.module; + return_symbol.base_name = symbol.base_name; + return_symbol.value = nil_exprt(); + return_symbol.type = to_code_type(symbol.type).return_type(); + + return_symbol.name = + id2string(symbol.name) + "." + id2string(symbol.base_name); + + return_symbol.pretty_name = strip_verilog_prefix(return_symbol.name); + + symbol_table.add(return_symbol); + } + + // collect symbols in the declarations within the task/function + for(auto &decl : decl.declarations()) + collect_symbols(decl); + + collect_symbols(decl.body()); + + function_or_task_name = ""; } else { diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp index 41dc70b89..58b858d13 100644 --- a/src/verilog/verilog_interfaces.cpp +++ b/src/verilog/verilog_interfaces.cpp @@ -136,227 +136,6 @@ void verilog_typecheckt::check_module_ports( /*******************************************************************\ -Function: verilog_typecheckt::interface_function_or_task - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void verilog_typecheckt::interface_function_or_task( - const verilog_declt &decl) -{ - irep_idt decl_class=decl.get_class(); - - // only add symbol for now - symbolt *new_symbol; - - { - symbolt symbol; - - symbol.mode=mode; - symbol.module=module_identifier; - symbol.value=decl; - - typet return_type; - - if(decl_class==ID_function) - return_type = convert_type(decl.type()); - else - return_type=empty_typet(); - - symbol.type = code_typet{{}, return_type}; - - symbol.base_name=decl.get_identifier(); - symbol.name = hierarchical_identifier(symbol.base_name); - symbol.pretty_name=strip_verilog_prefix(symbol.name); - - if(symbol_table.move(symbol, new_symbol)) - { - error().source_location = decl.source_location(); - error() << "symbol `" << symbol.base_name - << "' is already declared" << eom; - throw 0; - } - } - - function_or_task_name=new_symbol->name; - - // add a symbol for the return value of functions - - if(decl_class==ID_function) - { - symbolt return_symbol; - return_symbol.is_state_var=true; - return_symbol.is_lvalue=true; - return_symbol.mode=new_symbol->mode; - return_symbol.module=new_symbol->module; - return_symbol.base_name=new_symbol->base_name; - return_symbol.value.make_nil(); - return_symbol.type=to_code_type(new_symbol->type).return_type(); - - return_symbol.name= - id2string(new_symbol->name)+"."+ - id2string(new_symbol->base_name); - - return_symbol.pretty_name=strip_verilog_prefix(return_symbol.name); - - symbol_table.add(return_symbol); - } - - // do the declarations within the task/function - auto &declarations = decl.declarations(); - - for(auto &decl : declarations) - interface_function_or_task_decl(decl); - - interface_statement(decl.body()); - - function_or_task_name=""; -} - -/*******************************************************************\ - -Function: verilog_typecheckt::interface_function_or_task_decl - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void verilog_typecheckt::interface_function_or_task_decl(const verilog_declt &decl) -{ - symbolt symbol; - typet type; - bool input=false, output=false; - - symbol.mode=mode; - symbol.module=module_identifier; - symbol.value.make_nil(); - - const irep_idt &port_class=decl.get_class(); - - if( - port_class == ID_function || port_class == ID_task || - port_class == ID_verilog_genvar) - { - error().source_location = decl.source_location(); - error() << "this kind of declaration is not expected here" << eom; - throw 0; - } - else - { - type = convert_type(decl.type()); - - symbol.is_state_var=true; - - if(port_class==ID_input) - { - input=true; - } - else if(port_class==ID_output) - { - output=true; - } - else if(port_class==ID_output_register) - { - output=true; - } - else if(port_class==ID_inout) - { - input=true; - output=true; - } - else if(port_class == ID_reg || port_class == ID_var) - { - } - else if(port_class==ID_wire) - { - error().source_location = decl.source_location(); - error() << "wires are not allowed here" << eom; - throw 0; - } - else if(port_class == ID_typedef) - { - symbol.is_type = true; - } - else - { - if( - type.id() == ID_integer || type.id() == ID_verilog_realtime || - type.id() == ID_verilog_shortreal || type.id() == ID_verilog_real) - { - symbol.is_lvalue = true; - } - else - { - error().source_location = decl.source_location(); - error() << "unexpected port class: `" << port_class << '\'' << eom; - throw 0; - } - } - } - - for(auto &declarator : decl.declarators()) - { - DATA_INVARIANT(declarator.id() == ID_declarator, "must have declarator"); - - symbol.base_name = declarator.base_name(); - - if(symbol.base_name.empty()) - { - throw errort().with_location(decl.source_location()) - << "empty symbol name"; - } - - symbol.type = type; - - symbol.name = hierarchical_identifier(symbol.base_name); - - symbol.pretty_name=strip_verilog_prefix(symbol.name); - - if(input || output) - { - // Terminology clash: these aren't called 'parameters' - // in Verilog terminology, but inputs and outputs. - // We'll use the C terminology, and call them parameters. - // Not to be confused with module parameters. - auto s_it=symbol_table.get_writeable(function_or_task_name); - CHECK_RETURN(s_it!=nullptr); - symbolt &function_or_task_symbol=*s_it; - code_typet::parameterst ¶meters= - to_code_type(function_or_task_symbol.type).parameters(); - parameters.push_back(code_typet::parametert(symbol.type)); - code_typet::parametert ¶meter=parameters.back(); - parameter.set_base_name(symbol.base_name); - parameter.set_identifier(symbol.name); - parameter.set(ID_output, output); - parameter.set(ID_input, input); - } - - symbol_tablet::symbolst::const_iterator result= - symbol_table.symbols.find(symbol.name); - - if(result!=symbol_table.symbols.end()) - { - error().source_location = decl.source_location(); - error() << "symbol `" << symbol.base_name - << "' is already declared" << eom; - throw 0; - } - - symbol_table.add(symbol); - } -} - -/*******************************************************************\ - Function: verilog_typecheckt::interface_module_decl Inputs: @@ -383,7 +162,7 @@ void verilog_typecheckt::interface_module_decl( if(port_class==ID_function || port_class==ID_task) { - interface_function_or_task(decl); + // symbols already created during elaboration return; } else if( @@ -618,8 +397,6 @@ void verilog_typecheckt::interface_module_item( { if(function_or_task_name.empty()) interface_module_decl(to_verilog_decl(module_item)); - else - interface_function_or_task_decl(to_verilog_decl(module_item)); } else if(module_item.id()==ID_parameter_decl || module_item.id()==ID_local_parameter_decl) @@ -683,8 +460,6 @@ void verilog_typecheckt::interface_statement( { if(function_or_task_name.empty()) interface_module_decl(to_verilog_decl(statement)); - else - interface_function_or_task_decl(to_verilog_decl(statement)); } else if(statement.id()==ID_event_guard) { diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h index 43ababc73..d8c115539 100644 --- a/src/verilog/verilog_typecheck.h +++ b/src/verilog/verilog_typecheck.h @@ -116,7 +116,6 @@ class verilog_typecheckt: void module_interface(const verilog_module_sourcet &); void check_module_ports(const verilog_module_sourcet::port_listt &); void interface_module_decl(const class verilog_declt &); - void interface_function_or_task_decl(const class verilog_declt &); void interface_inst(const verilog_inst_baset &); void interface_inst( const verilog_inst_baset &, @@ -125,7 +124,6 @@ class verilog_typecheckt: void interface_block(const class verilog_blockt &); void interface_generate_block(const class verilog_generate_blockt &); void interface_statement(const class verilog_statementt &); - void interface_function_or_task(const class verilog_declt &); array_typet array_type( const irept &src,