Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit d0fa372

Browse files
committedJun 12, 2025·
introduce SMV enumeration type
SMV enumerations behave differently from enumeration_typet; hence, this introduces smv_enumeration_typet, which is subsequently lowered to enumeration_typet.
1 parent 5906108 commit d0fa372

File tree

7 files changed

+236
-102
lines changed

7 files changed

+236
-102
lines changed
 

‎src/hw_cbmc_irep_ids.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ IREP_ID_ONE(E)
1818
IREP_ID_ONE(G)
1919
IREP_ID_ONE(X)
2020
IREP_ID_ONE(smv_bitimplies)
21+
IREP_ID_ONE(smv_enumeration)
2122
IREP_ID_ONE(smv_extend)
2223
IREP_ID_ONE(smv_next)
2324
IREP_ID_ONE(smv_iff)

‎src/smvlang/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ SRC = smv_expr.cpp \
22
smv_language.cpp \
33
smv_parser.cpp \
44
smv_typecheck.cpp \
5+
smv_types.cpp \
56
expr2smv.cpp \
67
smv_y.tab.cpp \
78
lex.yy.cpp \

‎src/smvlang/expr2smv.cpp

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
1212
#include <util/mathematical_types.h>
1313

1414
#include "smv_expr.h"
15+
#include "smv_types.h"
1516

1617
/*******************************************************************\
1718
@@ -337,6 +338,12 @@ expr2smvt::resultt expr2smvt::convert_typecast(const typecast_exprt &expr)
337338
return convert_rec(smv_resize_exprt{expr.op(), dest_width, dest_type});
338339
}
339340
}
341+
else if(
342+
src_type.id() == ID_smv_enumeration && dest_type.id() == ID_smv_enumeration)
343+
{
344+
// added by SMV typechecker, implicit
345+
return convert_rec(expr.op());
346+
}
340347
else
341348
return convert_norep(expr);
342349
}
@@ -593,10 +600,9 @@ expr2smvt::resultt expr2smvt::convert_constant(const constant_exprt &src)
593600
else
594601
dest+="FALSE";
595602
}
596-
else if(type.id()==ID_integer ||
597-
type.id()==ID_natural ||
598-
type.id()==ID_range ||
599-
type.id()==ID_enumeration)
603+
else if(
604+
type.id() == ID_integer || type.id() == ID_natural ||
605+
type.id() == ID_range || type.id() == ID_smv_enumeration)
600606
{
601607
dest = id2string(src.get_value());
602608
}
@@ -885,15 +891,15 @@ std::string type2smv(const typet &type, const namespacet &ns)
885891
code += type2smv(to_array_type(type).element_type(), ns);
886892
return code;
887893
}
888-
else if(type.id()==ID_enumeration)
894+
else if(type.id() == ID_smv_enumeration)
889895
{
890-
const irept::subt &elements=to_enumeration_type(type).elements();
896+
auto elements = to_smv_enumeration_type(type).elements();
891897
std::string code = "{ ";
892898
bool first=true;
893899
for(auto &element : elements)
894900
{
895901
if(first) first=false; else code+=", ";
896-
code += element.id_string();
902+
code += id2string(element);
897903
}
898904
code+=" }";
899905
return code;

‎src/smvlang/parser.y

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -522,7 +522,7 @@ module_type_specifier:
522522

523523
enum_list : enum_element
524524
{
525-
init($$, ID_enumeration);
525+
init($$, ID_smv_enumeration);
526526
stack_expr($$).add(ID_elements).get_sub().push_back(irept(stack_expr($1).id()));
527527
}
528528
| enum_list ',' enum_element
@@ -808,7 +808,7 @@ variable_identifier: complex_identifier
808808
else if(is_enum)
809809
{
810810
init($$, ID_constant);
811-
stack_expr($$).type()=typet(ID_enumeration);
811+
stack_expr($$).type()=typet(ID_smv_enumeration);
812812
stack_expr($$).set(ID_value, id);
813813
}
814814
else // not an enum, probably a variable

‎src/smvlang/smv_typecheck.cpp

Lines changed: 70 additions & 93 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
1919
#include "expr2smv.h"
2020
#include "smv_expr.h"
2121
#include "smv_range.h"
22+
#include "smv_types.h"
2223

2324
#include <algorithm>
2425
#include <cassert>
@@ -82,8 +83,6 @@ class smv_typecheckt:public typecheckt
8283

8384
void check_type(const typet &);
8485
smv_ranget convert_type(const typet &);
85-
static bool
86-
is_contained_in(const enumeration_typet &, const enumeration_typet &);
8786

8887
void convert(smv_parse_treet::modulet::itemt &);
8988
void typecheck(smv_parse_treet::modulet::itemt &);
@@ -141,6 +140,8 @@ class smv_typecheckt:public typecheckt
141140

142141
void lower_node(exprt &) const;
143142

143+
void lower(typet &) const;
144+
144145
void lower(exprt &expr) const
145146
{
146147
expr.visit_post([this](exprt &expr) { lower_node(expr); });
@@ -149,40 +150,6 @@ class smv_typecheckt:public typecheckt
149150

150151
/*******************************************************************\
151152
152-
Function: smv_typecheckt::is_contained_in
153-
154-
Inputs:
155-
156-
Outputs:
157-
158-
Purpose:
159-
160-
\*******************************************************************/
161-
162-
bool smv_typecheckt::is_contained_in(
163-
const enumeration_typet &type1,
164-
const enumeration_typet &type2)
165-
{
166-
// This is quadratic.
167-
for(auto &element1 : type1.elements())
168-
{
169-
bool found = false;
170-
for(auto &element2 : type2.elements())
171-
if(element1.id() == element2.id())
172-
{
173-
found = true;
174-
break;
175-
}
176-
177-
if(!found)
178-
return false;
179-
}
180-
181-
return true;
182-
}
183-
184-
/*******************************************************************\
185-
186153
Function: smv_typecheckt::convert_ports
187154
188155
Inputs:
@@ -498,15 +465,15 @@ smv_ranget smv_typecheckt::convert_type(const typet &src)
498465
{
499466
return smv_ranget::from_type(to_range_type(src));
500467
}
501-
else if(src.id()==ID_enumeration)
468+
else if(src.id() == ID_smv_enumeration)
502469
{
503470
smv_ranget dest;
504471

505472
dest.from=0;
506473

507-
std::size_t number_of_elements=
508-
to_enumeration_type(src).elements().size();
509-
474+
std::size_t number_of_elements =
475+
to_smv_enumeration_type(src).elements().size();
476+
510477
if(number_of_elements==0)
511478
dest.to=0;
512479
else
@@ -556,36 +523,16 @@ typet smv_typecheckt::type_union(
556523
}
557524

558525
// both enums?
559-
if(type1.id()==ID_enumeration && type2.id()==ID_enumeration)
526+
if(type1.id() == ID_smv_enumeration && type2.id() == ID_smv_enumeration)
560527
{
561-
auto &e_type1 = to_enumeration_type(type1);
562-
auto &e_type2 = to_enumeration_type(type2);
563-
564-
if(is_contained_in(e_type2, e_type1))
565-
return type1;
566-
567-
if(is_contained_in(e_type1, e_type2))
568-
return type2;
569-
570-
// make union
571-
std::set<irep_idt> enum_set;
572-
573-
for(auto &e : e_type1.elements())
574-
enum_set.insert(e.id());
575-
576-
for(auto &e : e_type2.elements())
577-
enum_set.insert(e.id());
528+
auto &e_type1 = to_smv_enumeration_type(type1);
529+
auto &e_type2 = to_smv_enumeration_type(type2);
578530

579-
enumeration_typet union_type;
580-
union_type.elements().reserve(enum_set.size());
581-
for(auto &e : enum_set)
582-
union_type.elements().push_back(irept{e});
583-
584-
return std::move(union_type);
531+
return ::type_union(e_type1, e_type2);
585532
}
586533

587534
// one of them enum?
588-
if(type1.id() == ID_enumeration || type2.id() == ID_enumeration)
535+
if(type1.id() == ID_smv_enumeration || type2.id() == ID_smv_enumeration)
589536
{
590537
throw errort().with_location(source_location)
591538
<< "no type union for types " << to_string(type1) << " and "
@@ -868,10 +815,9 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
868815
mp_integer int_value = string2integer(id2string(value));
869816
expr.type() = range_typet{int_value, int_value};
870817
}
871-
else if(type.id() == ID_enumeration)
818+
else if(type.id() == ID_smv_enumeration)
872819
{
873-
auto t = enumeration_typet{};
874-
t.elements().push_back(irept{value});
820+
auto t = smv_enumeration_typet{{value}};
875821
expr.type() = std::move(t);
876822
}
877823
else if(type.id() == ID_bool)
@@ -1252,6 +1198,9 @@ Function: smv_typecheckt::lower_node
12521198

12531199
void smv_typecheckt::lower_node(exprt &expr) const
12541200
{
1201+
// lower the type
1202+
lower(expr.type());
1203+
12551204
if(expr.id() == ID_smv_extend)
12561205
{
12571206
auto &smv_extend = to_smv_extend_expr(expr);
@@ -1274,6 +1223,27 @@ void smv_typecheckt::lower_node(exprt &expr) const
12741223

12751224
/*******************************************************************\
12761225
1226+
Function: smv_typecheckt::lower
1227+
1228+
Inputs:
1229+
1230+
Outputs:
1231+
1232+
Purpose:
1233+
1234+
\*******************************************************************/
1235+
1236+
void smv_typecheckt::lower(typet &type) const
1237+
{
1238+
// lower the type
1239+
if(type.id() == ID_smv_enumeration)
1240+
{
1241+
type.id(ID_enumeration);
1242+
}
1243+
}
1244+
1245+
/*******************************************************************\
1246+
12771247
Function: smv_typecheckt::convert_expr_to
12781248
12791249
Inputs:
@@ -1340,35 +1310,40 @@ void smv_typecheckt::convert_expr_to(exprt &expr, const typet &type)
13401310
}
13411311
}
13421312
}
1343-
else if(type.id() == ID_enumeration)
1313+
else if(type.id() == ID_smv_enumeration)
13441314
{
1345-
auto &e_type = to_enumeration_type(type);
1315+
auto &e_type = to_smv_enumeration_type(type);
13461316

1347-
if(expr.id() == ID_constant && expr.type().id() == ID_enumeration)
1348-
{
1349-
if(is_contained_in(to_enumeration_type(expr.type()), e_type))
1350-
{
1351-
// re-type the constant
1352-
expr.type() = type;
1353-
return;
1354-
}
1355-
else
1356-
{
1357-
throw errort().with_location(expr.find_source_location())
1358-
<< "enum " << to_string(expr) << " not a member of "
1359-
<< to_string(type);
1360-
}
1361-
}
1362-
else if(expr.id() == ID_typecast)
1317+
if(expr.type().id() == ID_smv_enumeration)
13631318
{
1364-
// created by type unions
1365-
auto &op = to_typecast_expr(expr).op();
1366-
if(
1367-
expr.type().id() == ID_enumeration &&
1368-
op.type().id() == ID_enumeration)
1319+
// subset?
1320+
if(to_smv_enumeration_type(expr.type()).is_subset_of(e_type))
13691321
{
1370-
convert_expr_to(op, type);
1371-
expr = std::move(op);
1322+
// yes, it's a subset
1323+
if(expr.is_constant())
1324+
{
1325+
// re-type the constant
1326+
expr.type() = type;
1327+
return;
1328+
}
1329+
else if(expr.id() == ID_typecast)
1330+
{
1331+
// created by type unions
1332+
auto &op = to_typecast_expr(expr).op();
1333+
if(
1334+
expr.type().id() == ID_smv_enumeration &&
1335+
op.type().id() == ID_smv_enumeration)
1336+
{
1337+
convert_expr_to(op, type);
1338+
expr = std::move(op);
1339+
return;
1340+
}
1341+
}
1342+
else // anything else
1343+
{
1344+
expr = typecast_exprt{std::move(expr), type};
1345+
return;
1346+
}
13721347
}
13731348
}
13741349
}
@@ -1862,6 +1837,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
18621837
conjunction(trans_trans), module_symbol.type};
18631838

18641839
// lowering
1840+
lower(module_symbol.type);
18651841
lower(module_symbol.value);
18661842

18671843
module_symbol.pretty_name = strip_smv_prefix(module_symbol.name);
@@ -1902,6 +1878,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
19021878
spec_symbol.pretty_name = strip_smv_prefix(spec_symbol.name);
19031879

19041880
// lowering
1881+
lower(spec_symbol.type);
19051882
lower(spec_symbol.value);
19061883

19071884
symbol_table.add(spec_symbol);

‎src/smvlang/smv_types.cpp

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
/*******************************************************************\
2+
3+
Module: SMV Types
4+
5+
Author: Daniel Kroening, dkr@amazon.com
6+
7+
\*******************************************************************/
8+
9+
#include "smv_types.h"
10+
11+
#include <set>
12+
13+
smv_enumeration_typet::smv_enumeration_typet(
14+
const std::vector<irep_idt> &element_ids)
15+
: typet(ID_smv_enumeration)
16+
{
17+
auto &sub = elements_sub();
18+
for(auto &element_id : element_ids)
19+
sub.push_back(irept{element_id});
20+
}
21+
22+
std::vector<irep_idt> smv_enumeration_typet::elements() const
23+
{
24+
std::vector<irep_idt> result;
25+
26+
auto &elements_sub = find(ID_elements).get_sub();
27+
28+
result.reserve(elements_sub.size());
29+
30+
for(auto &e : elements_sub)
31+
result.push_back(e.id());
32+
33+
return result;
34+
}
35+
36+
bool smv_enumeration_typet::is_subset_of(
37+
const smv_enumeration_typet &other) const
38+
{
39+
// This is quadratic.
40+
for(auto &element1 : elements())
41+
{
42+
bool found = false;
43+
for(auto &element2 : other.elements())
44+
if(element1 == element2)
45+
{
46+
found = true;
47+
break;
48+
}
49+
50+
if(!found)
51+
return false;
52+
}
53+
54+
return true;
55+
}
56+
57+
smv_enumeration_typet type_union(
58+
const smv_enumeration_typet &e_type1,
59+
const smv_enumeration_typet &e_type2)
60+
{
61+
if(e_type2.is_subset_of(e_type1))
62+
return e_type1;
63+
64+
if(e_type1.is_subset_of(e_type2))
65+
return e_type2;
66+
67+
// make union
68+
std::set<irep_idt> enum_set;
69+
70+
for(auto &e : e_type1.elements())
71+
enum_set.insert(e);
72+
73+
for(auto &e : e_type2.elements())
74+
enum_set.insert(e);
75+
76+
// turn into vector
77+
std::vector<irep_idt> elements;
78+
79+
elements.reserve(enum_set.size());
80+
81+
for(auto &e : enum_set)
82+
elements.push_back(e);
83+
84+
return smv_enumeration_typet{std::move(elements)};
85+
}

‎src/smvlang/smv_types.h

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
/*******************************************************************\
2+
3+
Module: SMV Types
4+
5+
Author: Daniel Kroening, dkr@amazon.com
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_SMV_TYPES_H
10+
#define CPROVER_SMV_TYPES_H
11+
12+
#include <util/type.h>
13+
14+
/// The SMV enumerated type
15+
class smv_enumeration_typet : public typet
16+
{
17+
public:
18+
smv_enumeration_typet() : typet(ID_smv_enumeration)
19+
{
20+
}
21+
22+
explicit smv_enumeration_typet(const std::vector<irep_idt> &);
23+
24+
bool is_subset_of(const smv_enumeration_typet &) const;
25+
26+
// the ordering does not matter; this makes a copy
27+
std::vector<irep_idt> elements() const;
28+
29+
subt &elements_sub()
30+
{
31+
return add(ID_elements).get_sub();
32+
}
33+
};
34+
35+
/// compute the union of the given enumeration types
36+
smv_enumeration_typet
37+
type_union(const smv_enumeration_typet &, const smv_enumeration_typet &);
38+
39+
/*! \brief Cast a generic typet to a \ref smv_enumeration_typet
40+
*
41+
* This is an unchecked conversion. \a type must be known to be \ref
42+
* smv_enumeration_typet.
43+
*
44+
* \param type Source type
45+
* \return Object of type \ref smv_enumeration_typet
46+
*
47+
* \ingroup gr_std_types
48+
*/
49+
inline const smv_enumeration_typet &to_smv_enumeration_type(const typet &type)
50+
{
51+
PRECONDITION(type.id() == ID_smv_enumeration);
52+
return static_cast<const smv_enumeration_typet &>(type);
53+
}
54+
55+
/*! \copydoc to_smv_enumeration_type(const typet &)
56+
* \ingroup gr_std_types
57+
*/
58+
inline smv_enumeration_typet &to_smv_enumeration_type(typet &type)
59+
{
60+
PRECONDITION(type.id() == ID_smv_enumeration);
61+
return static_cast<smv_enumeration_typet &>(type);
62+
}
63+
64+
#endif // CPROVER_SMV_TYPES_H

0 commit comments

Comments
 (0)
Please sign in to comment.