Skip to content

Commit 665d640

Browse files
tautschnigtautschnig
authored
Merge pull request #1431 from diffblue/typename_h
Verilog: extract code for `$typename`, `$left`, `$right` into separate file
2 parents d801d57 + 91f3a22 commit 665d640

File tree

6 files changed

+211
-146
lines changed

6 files changed

+211
-146
lines changed

‎src/verilog/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ SRC = aval_bval_encoding.cpp \
22
convert_literals.cpp \
33
expr2verilog.cpp \
44
sva_expr.cpp \
5+
typename.cpp \
56
verilog_bits.cpp \
67
verilog_elaborate.cpp \
78
verilog_elaborate_type.cpp \

‎src/verilog/typename.cpp‎

Lines changed: 156 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,156 @@
1+
/*******************************************************************\
2+
3+
Module: $typename
4+
5+
Author: Daniel Kroening, dkr@amazon.com
6+
7+
\*******************************************************************/
8+
9+
#include "typename.h"
10+
11+
#include <util/arith_tools.h>
12+
13+
#include "verilog_bits.h"
14+
15+
// unpacked array: left bound
16+
// packed array: index of most significant element
17+
// 0 otherwise
18+
mp_integer verilog_left(const typet &type)
19+
{
20+
if(
21+
type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
22+
type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv ||
23+
type.id() == ID_bool)
24+
{
25+
auto offset = type.get_int(ID_C_offset);
26+
if(type.get_bool(ID_C_increasing))
27+
return offset;
28+
else
29+
return offset + verilog_bits(type) - 1;
30+
}
31+
else if(type.id() == ID_array)
32+
{
33+
auto offset = numeric_cast_v<mp_integer>(
34+
to_constant_expr(static_cast<const exprt &>(type.find(ID_offset))));
35+
if(type.get_bool(ID_C_increasing))
36+
return offset;
37+
else
38+
{
39+
return offset +
40+
numeric_cast_v<mp_integer>(
41+
to_constant_expr(to_array_type(type).size())) -
42+
1;
43+
}
44+
}
45+
else
46+
return 0;
47+
}
48+
49+
// unpacked array: right bound
50+
// packed array: index of least significant element
51+
// 0 otherwise
52+
mp_integer verilog_right(const typet &type)
53+
{
54+
if(
55+
type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
56+
type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv ||
57+
type.id() == ID_bool)
58+
{
59+
auto offset = type.get_int(ID_C_offset);
60+
if(type.get_bool(ID_C_increasing))
61+
return offset + verilog_bits(type) - 1;
62+
else
63+
return offset;
64+
}
65+
else if(type.id() == ID_array)
66+
{
67+
auto offset = numeric_cast_v<mp_integer>(
68+
to_constant_expr(static_cast<const exprt &>(type.find(ID_offset))));
69+
if(type.get_bool(ID_C_increasing))
70+
{
71+
return offset +
72+
numeric_cast_v<mp_integer>(
73+
to_constant_expr(to_array_type(type).size())) -
74+
1;
75+
}
76+
else
77+
return offset;
78+
}
79+
else
80+
return 0;
81+
}
82+
83+
std::string verilog_typename(const typet &type)
84+
{
85+
const auto verilog_type = type.get(ID_C_verilog_type);
86+
87+
auto left = [](const typet &type)
88+
{ return integer2string(verilog_left(type)); };
89+
auto right = [](const typet &type)
90+
{ return integer2string(verilog_right(type)); };
91+
92+
if(type.id() == ID_unsignedbv)
93+
{
94+
if(verilog_type == ID_verilog_byte)
95+
return "byte unsigned";
96+
else if(verilog_type == ID_verilog_int)
97+
return "int unsigned";
98+
else if(verilog_type == ID_verilog_longint)
99+
return "longint unsigned";
100+
else if(verilog_type == ID_verilog_shortint)
101+
return "shortint unsigned";
102+
else
103+
return "bit[" + left(type) + ":" + right(type) + "]";
104+
}
105+
else if(type.id() == ID_verilog_unsignedbv)
106+
{
107+
return "logic[" + left(type) + ":" + right(type) + "]";
108+
}
109+
else if(type.id() == ID_bool)
110+
{
111+
return "bit";
112+
}
113+
else if(type.id() == ID_signedbv)
114+
{
115+
if(verilog_type == ID_verilog_byte)
116+
return "byte";
117+
else if(verilog_type == ID_verilog_int)
118+
return "int";
119+
else if(verilog_type == ID_verilog_longint)
120+
return "longint";
121+
else if(verilog_type == ID_verilog_shortint)
122+
return "shortint";
123+
else
124+
return "bit signed[" + left(type) + ":" + right(type) + "]";
125+
}
126+
else if(type.id() == ID_verilog_signedbv)
127+
{
128+
return "logic signed[" + left(type) + ":" + right(type) + "]";
129+
}
130+
else if(type.id() == ID_verilog_realtime)
131+
{
132+
return "realtime";
133+
}
134+
else if(type.id() == ID_verilog_real)
135+
{
136+
return "real";
137+
}
138+
else if(type.id() == ID_verilog_shortreal)
139+
{
140+
return "shortreal";
141+
}
142+
else if(type.id() == ID_verilog_chandle)
143+
{
144+
return "chandle";
145+
}
146+
else if(type.id() == ID_verilog_event)
147+
{
148+
return "event";
149+
}
150+
else if(type.id() == ID_verilog_string)
151+
{
152+
return "string";
153+
}
154+
else
155+
return "?";
156+
}

‎src/verilog/typename.h‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
/*******************************************************************\
2+
3+
Module: $typename
4+
5+
Author: Daniel Kroening, dkr@amazon.com
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_VERILOG_TYPENAME_H
10+
#define CPROVER_VERILOG_TYPENAME_H
11+
12+
#include <util/mp_arith.h>
13+
14+
class typet;
15+
16+
/// Verilog's $left
17+
mp_integer verilog_left(const typet &);
18+
19+
/// Verilog's $right
20+
mp_integer verilog_right(const typet &);
21+
22+
/// Verilog's $typename
23+
std::string verilog_typename(const typet &);
24+
25+
#endif

‎src/verilog/verilog_typecheck_expr.cpp‎

Lines changed: 5 additions & 146 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
2323
#include "aval_bval_encoding.h"
2424
#include "convert_literals.h"
2525
#include "expr2verilog.h"
26+
#include "typename.h"
2627
#include "verilog_bits.h"
2728
#include "verilog_expr.h"
2829
#include "verilog_lowering.h"
@@ -746,40 +747,7 @@ Function: verilog_typecheck_exprt::left
746747

747748
constant_exprt verilog_typecheck_exprt::left(const exprt &expr)
748749
{
749-
// unpacked array: left bound
750-
// packed array: index of most significant element
751-
// 0 otherwise
752-
auto left = [](const typet &type) -> mp_integer {
753-
if(
754-
type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
755-
type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv ||
756-
type.id() == ID_bool)
757-
{
758-
auto offset = type.get_int(ID_C_offset);
759-
if(type.get_bool(ID_C_increasing))
760-
return offset;
761-
else
762-
return offset + get_width(type) - 1;
763-
}
764-
else if(type.id() == ID_array)
765-
{
766-
auto offset = numeric_cast_v<mp_integer>(
767-
to_constant_expr(static_cast<const exprt &>(type.find(ID_offset))));
768-
if(type.get_bool(ID_C_increasing))
769-
return offset;
770-
else
771-
{
772-
return offset +
773-
numeric_cast_v<mp_integer>(
774-
to_constant_expr(to_array_type(type).size())) -
775-
1;
776-
}
777-
}
778-
else
779-
return 0;
780-
};
781-
782-
return from_integer(left(expr.type()), integer_typet{});
750+
return from_integer(verilog_left(expr.type()), integer_typet{});
783751
}
784752

785753
/*******************************************************************\
@@ -796,40 +764,7 @@ Function: verilog_typecheck_exprt::right
796764

797765
constant_exprt verilog_typecheck_exprt::right(const exprt &expr)
798766
{
799-
// unpacked array: right bound
800-
// packed array: index of least significant element
801-
// 0 otherwise
802-
auto right = [](const typet &type) -> mp_integer {
803-
if(
804-
type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
805-
type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv ||
806-
type.id() == ID_bool)
807-
{
808-
auto offset = type.get_int(ID_C_offset);
809-
if(type.get_bool(ID_C_increasing))
810-
return offset + get_width(type) - 1;
811-
else
812-
return offset;
813-
}
814-
else if(type.id() == ID_array)
815-
{
816-
auto offset = numeric_cast_v<mp_integer>(
817-
to_constant_expr(static_cast<const exprt &>(type.find(ID_offset))));
818-
if(type.get_bool(ID_C_increasing))
819-
{
820-
return offset +
821-
numeric_cast_v<mp_integer>(
822-
to_constant_expr(to_array_type(type).size())) -
823-
1;
824-
}
825-
else
826-
return offset;
827-
}
828-
else
829-
return 0;
830-
};
831-
832-
return from_integer(right(expr.type()), integer_typet{});
767+
return from_integer(verilog_right(expr.type()), integer_typet{});
833768
}
834769

835770
/*******************************************************************\
@@ -950,84 +885,8 @@ Function: verilog_typecheck_exprt::typename_string
950885

951886
exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
952887
{
953-
auto &type = expr.type();
954-
955-
auto left = this->left(expr);
956-
auto right = this->right(expr);
957-
958-
const auto verilog_type = type.get(ID_C_verilog_type);
959-
960-
std::string s;
961-
962-
if(type.id() == ID_unsignedbv)
963-
{
964-
if(verilog_type == ID_verilog_byte)
965-
s = "byte unsigned";
966-
else if(verilog_type == ID_verilog_int)
967-
s = "int unsigned";
968-
else if(verilog_type == ID_verilog_longint)
969-
s = "longint unsigned";
970-
else if(verilog_type == ID_verilog_shortint)
971-
s = "shortint unsigned";
972-
else
973-
s = "bit[" + to_string(left) + ":" + to_string(right) + "]";
974-
}
975-
else if(type.id() == ID_verilog_unsignedbv)
976-
{
977-
s = "logic[" + to_string(left) + ":" + to_string(right) + "]";
978-
}
979-
else if(type.id() == ID_bool)
980-
{
981-
s = "bit";
982-
}
983-
else if(type.id() == ID_signedbv)
984-
{
985-
if(verilog_type == ID_verilog_byte)
986-
s = "byte";
987-
else if(verilog_type == ID_verilog_int)
988-
s = "int";
989-
else if(verilog_type == ID_verilog_longint)
990-
s = "longint";
991-
else if(verilog_type == ID_verilog_shortint)
992-
s = "shortint";
993-
else
994-
s = "bit signed[" + to_string(left) + ":" + to_string(right) + "]";
995-
}
996-
else if(type.id() == ID_verilog_signedbv)
997-
{
998-
s = "logic signed[" + to_string(left) + ":" + to_string(right) + "]";
999-
}
1000-
else if(type.id() == ID_verilog_realtime)
1001-
{
1002-
s = "realtime";
1003-
}
1004-
else if(type.id() == ID_verilog_real)
1005-
{
1006-
s = "real";
1007-
}
1008-
else if(type.id() == ID_verilog_shortreal)
1009-
{
1010-
s = "shortreal";
1011-
}
1012-
else if(type.id() == ID_verilog_chandle)
1013-
{
1014-
s = "chandle";
1015-
}
1016-
else if(type.id() == ID_verilog_event)
1017-
{
1018-
s = "event";
1019-
}
1020-
else if(type.id() == ID_verilog_string)
1021-
{
1022-
s = "string";
1023-
}
1024-
else
1025-
s = "?";
1026-
1027-
auto result = convert_string_literal(s);
1028-
result.add_source_location() = expr.source_location();
1029-
1030-
return std::move(result);
888+
auto s = verilog_typename(expr.type());
889+
return convert_string_literal(s).with_source_location(expr);
1031890
}
1032891

1033892
/*******************************************************************\

‎unit/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ SRC += smvlang/expr2smv.cpp \
1111
temporal-logic/sva_to_ltl.cpp \
1212
temporal-logic/nnf.cpp \
1313
temporal-logic/trivial_sva.cpp \
14+
verilog/typename.cpp \
1415
# Empty last line
1516

1617
INCLUDES= -I ../src/ -I . -I $(CPROVER_DIR)/unit -I $(CPROVER_DIR)/src

0 commit comments

Comments
 (0)