Skip to content

Commit

Permalink
Merge pull request #753 from diffblue/parameters10
Browse files Browse the repository at this point in the history
Verilog: reject non-constant parameters
  • Loading branch information
tautschnig authored Oct 7, 2024
2 parents 8bbc75e + 995f6b4 commit aeecd2e
Show file tree
Hide file tree
Showing 6 changed files with 68 additions and 16 deletions.
7 changes: 7 additions & 0 deletions regression/verilog/enums/enum5.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE
enum5.sv
--bound 0
^file .* line 6: expected constant expression, but got `main\.some_wire'$
^EXIT=2$
^SIGNAL=0$
--
8 changes: 8 additions & 0 deletions regression/verilog/enums/enum5.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
module main;

wire some_wire;

// some_wire is not a constant
typedef enum bit [7:0] { A = some_wire } enum_t;

endmodule
13 changes: 11 additions & 2 deletions src/verilog/verilog_elaborate.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -614,6 +614,8 @@ void verilog_typecheckt::collect_symbols(const verilog_lett &let)
new_symbol.base_name = base_name;
new_symbol.pretty_name = strip_verilog_prefix(new_symbol.name);

let_symbols.insert(new_symbol.name);

add_symbol(std::move(new_symbol));
}

Expand Down Expand Up @@ -929,12 +931,17 @@ void verilog_typecheckt::elaborate_symbol_rec(irep_idt identifier)
// mark as "elaborating" to detect cycles
symbol.type.id(ID_elaborating);

bool is_let = let_symbols.find(symbol.name) != let_symbols.end();

// Is the type derived from the value (e.g., parameters)?
if(to_type_with_subtype(symbol.type).subtype().id() == ID_derive_from_value)
{
// First elaborate the value, possibly recursively.
convert_expr(symbol.value);
symbol.value = elaborate_constant_expression(symbol.value);

if(!is_let)
symbol.value = elaborate_constant_expression_check(symbol.value);

symbol.type = symbol.value.type();
}
else
Expand All @@ -948,7 +955,9 @@ void verilog_typecheckt::elaborate_symbol_rec(irep_idt identifier)
if(symbol.value.is_not_nil())
{
convert_expr(symbol.value);
symbol.value = elaborate_constant_expression(symbol.value);

if(!is_let)
symbol.value = elaborate_constant_expression_check(symbol.value);

// Cast to the given type.
propagate_type(symbol.value, symbol.type);
Expand Down
1 change: 1 addition & 0 deletions src/verilog/verilog_typecheck.h
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,7 @@ class verilog_typecheckt:
collect_symbols(const typet &, const verilog_parameter_declt::declaratort &);
void collect_port_symbols(const verilog_declt &);
std::vector<irep_idt> symbols_added;
std::set<irep_idt> let_symbols;

// instances
irep_idt parameterize_module(
Expand Down
54 changes: 40 additions & 14 deletions src/verilog/verilog_typecheck_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -844,13 +844,8 @@ exprt verilog_typecheck_exprt::convert_system_function(

if(arguments.size() >= 2)
{
auto tmp = elaborate_constant_expression(arguments[1]);
if(!tmp.is_constant())
{
throw errort().with_location(arguments[1].source_location())
<< "expected elaboration-time constant, but got `" << to_string(tmp)
<< '\'';
}
auto tmp = elaborate_constant_expression_check(arguments[1]);
arguments[1] = tmp;
}

expr.type() = arguments.front().type();
Expand Down Expand Up @@ -1454,12 +1449,12 @@ verilog_typecheck_exprt::convert_integer_constant_expression(exprt expr)
// this could be large
propagate_type(expr, integer_typet());

exprt tmp = elaborate_constant_expression(expr);
exprt tmp = elaborate_constant_expression_check(expr);

if(!tmp.is_constant())
if(tmp.id() == ID_infinity)
{
throw errort().with_location(source_location)
<< "expected constant expression, but got `" << to_string(tmp) << '\'';
<< "expected integer constant, but got $";
}

const auto &tmp_constant = to_constant_expr(tmp);
Expand Down Expand Up @@ -1515,6 +1510,9 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression(exprt expr)

if(symbol.is_macro)
{
// Elaborate recursively
elaborate_symbol_rec(symbol.name);

// A parameter or local parameter. Replace by its value.
return symbol.value;
}
Expand All @@ -1524,12 +1522,12 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression(exprt expr)
#if 0
status() << "READ " << identifier << " = " << to_string(value) << eom;
#endif

if(value.is_not_nil())
{
source_locationt source_location=expr.source_location();
exprt tmp=value;
tmp.add_source_location()=source_location;
source_locationt source_location = expr.source_location();
exprt tmp = value;
tmp.add_source_location() = source_location;
return tmp;
}
else
Expand Down Expand Up @@ -1671,6 +1669,34 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression(exprt expr)

/*******************************************************************\
Function: verilog_typecheck_exprt::elaborate_constant_expression_check
Inputs:
Outputs:
Purpose:
\*******************************************************************/

exprt verilog_typecheck_exprt::elaborate_constant_expression_check(exprt expr)
{
source_locationt source_location = expr.find_source_location();

exprt tmp = elaborate_constant_expression(std::move(expr));

// $ counts as a constant
if(!tmp.is_constant() && tmp.id() != ID_infinity)
{
throw errort().with_location(source_location)
<< "expected constant expression, but got `" << to_string(tmp) << '\'';
}

return tmp;
}

/*******************************************************************\
Function: verilog_typecheck_exprt::elaborate_constant_system_function_call
Inputs:
Expand Down
1 change: 1 addition & 0 deletions src/verilog/verilog_typecheck_expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -148,6 +148,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
bool is_constant_expression(const exprt &, mp_integer &value);
std::optional<mp_integer> is_constant_integer_post_convert(const exprt &);
exprt elaborate_constant_expression(exprt);
exprt elaborate_constant_expression_check(exprt);

// To be overridden, requires a Verilog interpreter.
virtual exprt elaborate_constant_function_call(const function_call_exprt &)
Expand Down

0 comments on commit aeecd2e

Please sign in to comment.