Skip to content

Commit bb75939

Browse files
kroeningkroening
authored
Merge pull request #371 from diffblue/strong-enum-typing
Verilog: strong typing for enums
2 parents 63c6f4b + 32329e3 commit bb75939

13 files changed

+111
-35
lines changed

‎regression/verilog/data-types/enum2.desc

+3-4
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
1-
KNOWNBUG
1+
CORE
22
enum2.sv
33

4-
^EXIT=10$
4+
^file .* line 4: assignment to enum requires enum of the same type$
5+
^EXIT=2$
56
^SIGNAL=0$
67
--
7-
--
8-
enum constants must be strongly typed.

‎regression/verilog/data-types/enum4.desc

+3-5
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,7 @@
1-
KNOWNBUG
1+
CORE
22
enum4.sv
33
--bound 0
4-
^EXIT=10$
4+
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main\.property\.p1\] always main\.my_light != 0 \+ 1 \+ 1 \+ 1: PROVED up to bound 0$
6+
^\[main\.property\.p1\] always 1 == 1: PROVED up to bound 0$
77
--
8-
--
9-
Type conversion not working

‎regression/verilog/data-types/enum_base_type1.desc

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
enum_base_type1.sv
3+
--bound 0
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[.*\] always 8 == 8: PROVED up to bound 0$
7+
--

‎regression/verilog/data-types/enum_base_type1.sv

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
module main;
2+
3+
typedef enum bit [7:0] { A } enum_t;
4+
5+
// expected to pass
6+
p1: assert property ($bits(A) == 8);
7+
8+
endmodule

‎regression/verilog/data-types/enum_cast1.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
enum_cast1.sv
3+
--bound 0
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.property\.p1\] always 1 == 1: PROVED up to bound 0$
7+
^\[main\.property\.p2\] always 2 == 2: PROVED up to bound 0$
8+
--

‎regression/verilog/data-types/enum_cast1.sv

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
module main;
2+
3+
typedef enum { A = 1, B = 2 } enum_t;
4+
5+
// expected to pass
6+
p1: assert property (A == enum_t'(1));
7+
p2: assert property (B == enum_t'(2));
8+
9+
endmodule

‎src/hw_cbmc_irep_ids.h

+1
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,7 @@ IREP_ID_ONE(uwire)
106106
IREP_ID_ONE(wand)
107107
IREP_ID_ONE(automatic)
108108
IREP_ID_ONE(verilog_enum)
109+
IREP_ID_TWO(C_verilog_type, #verilog_type)
109110
IREP_ID_ONE(verilog_type_reference)
110111
IREP_ID_ONE(enum_names)
111112
IREP_ID_ONE(var)

‎src/verilog/parser.y

+9-2
Original file line numberDiff line numberDiff line change
@@ -1253,6 +1253,11 @@ data_type:
12531253
init($$, ID_verilog_enum);
12541254
stack_type($$).add_subtype() = std::move(stack_type($2));
12551255
stack_type($$).set(ID_enum_names, stack_type($4));
1256+
1257+
// We attach a dummy id to distinguish two syntactically
1258+
// identical enum types.
1259+
auto id = PARSER.current_scope->prefix + "enum-" + PARSER.get_next_id();
1260+
stack_expr($$).set(ID_identifier, id);
12561261
}
12571262
| TOK_STRING
12581263
{ init($$, ID_string); }
@@ -1328,7 +1333,9 @@ enum_base_type_opt:
13281333
{ init($$, ID_nil); }
13291334
| integer_atom_type signing_opt
13301335
| integer_vector_type signing_opt packed_dimension_opt
1336+
{ $$ = $3; add_as_subtype(stack_type($$), stack_type($1)); }
13311337
| type_identifier packed_dimension_opt
1338+
{ $$ = $2; add_as_subtype(stack_type($$), stack_type($1)); }
13321339
;
13331340

13341341
non_integer_type:
@@ -2125,7 +2132,7 @@ gate_instance:
21252132

21262133
name_of_gate_instance_opt:
21272134
/* Optional */
2128-
{ init($$, "$_&#ANON" + PARSER.get_dummy_id()); }
2135+
{ init($$, "$_&#ANON" + PARSER.get_next_id()); }
21292136
| name_of_gate_instance
21302137
;
21312138

@@ -2192,7 +2199,7 @@ module_instance:
21922199
;
21932200

21942201
name_of_instance:
2195-
{ init($$, "$_&#ANON" + PARSER.get_dummy_id());}
2202+
{ init($$, "$_&#ANON" + PARSER.get_next_id());}
21962203
| TOK_NON_TYPE_IDENTIFIER
21972204
;
21982205

‎src/verilog/verilog_elaborate.cpp

+11-8
Original file line numberDiff line numberDiff line change
@@ -102,9 +102,8 @@ void verilog_typecheckt::collect_symbols(const typet &type)
102102
if(enum_type.has_base_type())
103103
collect_symbols(enum_type.base_type());
104104

105-
// The default base type is 'int'.
106-
auto base_type =
107-
enum_type.has_base_type() ? enum_type.base_type() : signedbv_typet(32);
105+
// convert the type now
106+
auto converted_type = convert_type(enum_type);
108107

109108
// Add the enum names to the symbol table for subsequent elaboration.
110109
// Values are given, or the previous plus one, starting with value '0'.
@@ -113,13 +112,17 @@ void verilog_typecheckt::collect_symbols(const typet &type)
113112
for(auto &enum_name : enum_type.enum_names())
114113
{
115114
if(enum_name.value().is_not_nil())
116-
initializer = enum_name.value();
115+
{
116+
exprt tmp = enum_name.value();
117+
convert_expr(tmp);
118+
initializer = std::move(tmp);
119+
}
117120

118-
exprt value = typecast_exprt(initializer, base_type);
121+
exprt value = typecast_exprt(initializer, converted_type);
119122

120123
const auto base_name = enum_name.base_name();
121124
const auto identifier = hierarchical_identifier(base_name);
122-
symbolt enum_name_symbol(identifier, base_type, mode);
125+
symbolt enum_name_symbol(identifier, converted_type, mode);
123126
enum_name_symbol.module = module_identifier;
124127
enum_name_symbol.base_name = base_name;
125128
enum_name_symbol.value = std::move(value);
@@ -128,8 +131,8 @@ void verilog_typecheckt::collect_symbols(const typet &type)
128131
add_symbol(std::move(enum_name_symbol));
129132

130133
initializer = plus_exprt(
131-
typecast_exprt(initializer, base_type),
132-
typecast_exprt(from_integer(1, integer_typet()), base_type));
134+
typecast_exprt(initializer, converted_type),
135+
typecast_exprt(from_integer(1, integer_typet()), converted_type));
133136
}
134137
}
135138
}

‎src/verilog/verilog_parser.h

+6-5
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,6 @@ class verilog_parsert:public parsert
4646

4747
verilog_parsert():mode(VIS_VERILOG)
4848
{
49-
dummy_id=0;
5049
}
5150

5251
// parser scopes and identifiers
@@ -118,12 +117,14 @@ class verilog_parsert:public parsert
118117
return scope_ptr == nullptr ? false : scope_ptr->is_type;
119118
}
120119

121-
unsigned dummy_id;
120+
// These are used for anonymous gate instances
121+
// and to create a unique identifier for enum types.
122+
std::size_t next_id_counter = 0;
122123

123-
std::string get_dummy_id()
124+
std::string get_next_id()
124125
{
125-
dummy_id++;
126-
return integer2string(dummy_id-1);
126+
next_id_counter++;
127+
return integer2string(next_id_counter - 1);
127128
}
128129
};
129130

‎src/verilog/verilog_typecheck_expr.cpp

+35-4
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,21 @@ void verilog_typecheck_exprt::propagate_type(
9494
exprt &expr,
9595
const typet &type)
9696
{
97+
auto &verilog_dest_type = type.get(ID_C_verilog_type);
98+
if(verilog_dest_type == ID_verilog_enum)
99+
{
100+
// IEEE 1800-2017 6.19.3: "a variable of type enum cannot be directly
101+
// assigned a value that lies outside the enumeration set unless an
102+
// explicit cast is used"
103+
if(
104+
expr.type().get(ID_C_verilog_type) != ID_verilog_enum ||
105+
expr.type().get(ID_C_identifier) != type.get(ID_C_identifier))
106+
{
107+
throw errort().with_location(expr.source_location())
108+
<< "assignment to enum requires enum of the same type";
109+
}
110+
}
111+
97112
if(expr.type()==type)
98113
return;
99114

@@ -193,7 +208,7 @@ void verilog_typecheck_exprt::propagate_type(
193208
}
194209
}
195210

196-
typecast(expr, type);
211+
implicit_typecast(expr, type);
197212
}
198213

199214
/*******************************************************************\
@@ -1436,7 +1451,7 @@ bool verilog_typecheck_exprt::is_constant_expression(
14361451

14371452
/*******************************************************************\
14381453
1439-
Function: verilog_typecheck_exprt::typecast
1454+
Function: verilog_typecheck_exprt::implicit_typecast
14401455
14411456
Inputs:
14421457
@@ -1446,13 +1461,28 @@ Function: verilog_typecheck_exprt::typecast
14461461
14471462
\*******************************************************************/
14481463

1449-
void verilog_typecheck_exprt::typecast(
1464+
void verilog_typecheck_exprt::implicit_typecast(
14501465
exprt &expr,
14511466
const typet &dest_type)
14521467
{
14531468
if(dest_type.id()==irep_idt())
14541469
return;
14551470

1471+
auto &verilog_dest_type = dest_type.get(ID_C_verilog_type);
1472+
if(verilog_dest_type == ID_verilog_enum)
1473+
{
1474+
// IEEE 1800-2017 6.19.3: "a variable of type enum cannot be directly
1475+
// assigned a value that lies outside the enumeration set unless an
1476+
// explicit cast is used"
1477+
if(
1478+
expr.type().get(ID_C_verilog_type) != ID_verilog_enum ||
1479+
expr.type().get(ID_C_identifier) != dest_type.get(ID_C_identifier))
1480+
{
1481+
throw errort().with_location(expr.source_location())
1482+
<< "assignment to enum requires enum of the same type";
1483+
}
1484+
}
1485+
14561486
if(expr.type()==dest_type)
14571487
return;
14581488

@@ -1800,7 +1830,8 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
18001830
}
18011831
else if(expr.id() == ID_typecast)
18021832
{
1803-
// System Verilog has got type'(expr).
1833+
// System Verilog has got type'(expr). This is an explicit
1834+
// type cast.
18041835
expr.type() = convert_type(expr.type());
18051836
convert_expr(expr.op());
18061837
}

‎src/verilog/verilog_typecheck_expr.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
130130
[[nodiscard]] exprt convert_extractbit_expr(extractbit_exprt);
131131
[[nodiscard]] exprt convert_replication_expr(replication_exprt);
132132
[[nodiscard]] exprt convert_shl_expr(shl_exprt);
133-
void typecast(exprt &, const typet &type);
133+
void implicit_typecast(exprt &, const typet &type);
134134
void tc_binary_expr(exprt &);
135135
void tc_binary_expr(const exprt &expr, exprt &op0, exprt &op1);
136136
void no_bool_ops(exprt &);

‎src/verilog/verilog_typecheck_type.cpp

+10-6
Original file line numberDiff line numberDiff line change
@@ -105,11 +105,14 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
105105
}
106106
else if(src.id() == ID_verilog_enum)
107107
{
108-
// Replace by base type.
108+
// Replace by base type, but annotate the original type.
109109
// The default base type is 'int'.
110110
auto &enum_type = to_verilog_enum_type(src);
111-
auto result =
112-
enum_type.has_base_type() ? enum_type.base_type() : signedbv_typet(32);
111+
auto result = enum_type.has_base_type()
112+
? convert_type(enum_type.base_type())
113+
: signedbv_typet(32);
114+
result.set(ID_C_verilog_type, ID_verilog_enum);
115+
result.set(ID_C_identifier, enum_type.identifier());
113116
return result.with_source_location(source_location);
114117
}
115118
else if(src.id() == ID_array)
@@ -130,9 +133,10 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
130133
? static_cast<const type_with_subtypet &>(src).subtype()
131134
: typet(ID_nil);
132135

133-
if(subtype.is_nil() ||
134-
subtype.id()==ID_signed ||
135-
subtype.id()==ID_unsigned)
136+
if(
137+
subtype.is_nil() || subtype.id() == ID_signed ||
138+
subtype.id() == ID_unsigned || subtype.id() == ID_verilog_bit ||
139+
subtype.id() == ID_verilog_logic)
136140
{
137141
// we have a bit-vector type, not an array
138142

0 commit comments

Comments
 (0)