replica
/
diffblue-hw-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #361 from diffblue/elaborate-functions 

Verilog: elaborate functions and tasks
This commit is contained in:
Daniel Kroening 2024-02-01 11:00:41 -08:00 committed by GitHub
parent ccb269ce7a d5ec4f0fb2
commit 93323f0178
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
5 changed files with 201 additions and 298 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
regression/verilog/functioncall/functioncall_as_constant1.desc
View File

@ -1,4 +1,4 @@
KNOWNBUG
CORE
functioncall_as_constant1.v
--module main --bound 0
^EXIT=0$

3
regression/verilog/functioncall/functioncall_as_constant1.v
View File

@ -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;

265
src/verilog/verilog_elaborate.cpp
View File

@ -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;
symbolt symbol;
symbol.mode = mode;
symbol.module = module_identifier;
symbol.value.make_nil();
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)
// If these are inputs/outputs of a function/task, then
// adjust the function/task signature.
if(function_or_task_name.empty())
{
symbol.is_output = true;
symbol.is_state_var = true;
}
else if(decl_class == ID_inout)
{
symbol.is_input = true;
symbol.is_output = true;
}
symbolt symbol;
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
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)
{
throw errort().with_location(declarator.source_location())
<< "unexpected type on declarator";
symbol.is_output = true;
symbol.is_state_var = true;
}
else if(decl_class == ID_inout)
{
symbol.is_input = true;
symbol.is_output = true;
}
if(symbol.base_name.empty())
for(auto &declarator : decl.declarators())
{
throw errort().with_location(decl.source_location())
<< "empty symbol name";
}
DATA_INVARIANT(
declarator.id() == ID_declarator, "must have declarator");
symbol.name = hierarchical_identifier(symbol.base_name);
symbol.pretty_name = strip_verilog_prefix(symbol.name);
symbol.base_name = declarator.base_name();
symbol.location = declarator.source_location();
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)
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())
<< "port `" << symbol.base_name
<< "' is declared both as input and as register";
<< "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
{
symbolt symbol;
bool input = false, output = false;
symbol.mode = mode;
symbol.module = module_identifier;
symbol.value.make_nil();
auto type = convert_type(decl.type());
symbol.is_state_var = true;
if(decl_class == ID_input)
{
input = true;
}
else if(decl_class == ID_output)
{
output = true;
}
else if(decl_class == ID_output_register)
{
output = true;
}
else if(decl_class == ID_inout)
{
input = true;
output = true;
}
symbols_added.push_back(symbol.name);
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.
symbolt &function_or_task_symbol =
symbol_table.get_writeable_ref(function_or_task_name);
code_typet::parameterst &parameters =
to_code_type(function_or_task_symbol.type).parameters();
parameters.push_back(code_typet::parametert(symbol.type));
code_typet::parametert &parameter = parameters.back();
parameter.set_base_name(symbol.base_name);
parameter.set_identifier(symbol.name);
parameter.set(ID_output, output);
parameter.set(ID_input, input);
}
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
{

227
src/verilog/verilog_interfaces.cpp
View File

@ -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 &parameters=
to_code_type(function_or_task_symbol.type).parameters();
parameters.push_back(code_typet::parametert(symbol.type));
code_typet::parametert &parameter=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)
{

2
src/verilog/verilog_typecheck.h
View File

@ -116,7 +116,6 @@ protected:
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 @@ protected:
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,