Skip to content

Commit 7c7e7e2

Browse files
tautschnigtautschnig
authored
Merge pull request #876 from diffblue/verilog-explicit-casts
SystemVerilog: IDs and classes for the explicit casts
2 parents 02b08f1 + 178e6d1 commit 7c7e7e2

File tree

8 files changed

+259
-60
lines changed

8 files changed

+259
-60
lines changed

‎regression/verilog/expressions/signing_cast1.desc‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
1-
KNOWNBUG
1+
CORE broken-smt-backend
22
signing_cast1.sv
33
--module main --bound 0
4-
^\[main\.p0\] always signed \[0:0\]'\(1'b1\) == -1: PROVED up to bound 0$
5-
^\[main\.p1\] always signed \[0:0\]'\(4'b1110\) == -2: PROVED up to bound 0$
6-
^\[main\.p2\] always signed \[0:0\]'\(4'b0111\) == 7: PROVED up to bound 0$
7-
^\[main\.p3\] always signed \[0:0\]'\(!0\) == -1: PROVED up to bound 0$
8-
^\[main\.p4\] always \[0:0\]'\(!0\) == 1: PROVED up to bound 0$
9-
^\[main\.p5\] always \[0:0\]'\(-1\) == 32'hFFFFFFFF: PROVED up to bound 0$
4+
^\[main\.p0\] always signed'\(1'b1\) == -1: PROVED up to bound 0$
5+
^\[main\.p1\] always signed'\(4'b1110\) == -2: PROVED up to bound 0$
6+
^\[main\.p2\] always signed'\(4'b0111\) == 7: PROVED up to bound 0$
7+
^\[main\.p3\] always signed'\(!0\) == -1: PROVED up to bound 0$
8+
^\[main\.p4\] always unsigned'\(!0\) == 1: PROVED up to bound 0$
9+
^\[main\.p5\] always unsigned'\(-1\) == 32'hFFFFFFFF: PROVED up to bound 0$
1010
^EXIT=0$
1111
^SIGNAL=0$
1212
--

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -83,8 +83,10 @@ IREP_ID_ONE(verilog_logical_equality)
8383
IREP_ID_ONE(verilog_logical_inequality)
8484
IREP_ID_ONE(verilog_wildcard_equality)
8585
IREP_ID_ONE(verilog_wildcard_inequality)
86-
IREP_ID_ONE(verilog_explicit_cast)
87-
IREP_ID_ONE(verilog_size_cast)
86+
IREP_ID_ONE(verilog_explicit_const_cast)
87+
IREP_ID_ONE(verilog_explicit_signing_cast)
88+
IREP_ID_ONE(verilog_explicit_size_cast)
89+
IREP_ID_ONE(verilog_explicit_type_cast)
8890
IREP_ID_ONE(verilog_implicit_typecast)
8991
IREP_ID_ONE(verilog_inside)
9092
IREP_ID_ONE(verilog_unique)

‎src/verilog/expr2verilog.cpp‎

Lines changed: 57 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -694,7 +694,7 @@ expr2verilogt::convert_typecast(const typecast_exprt &src)
694694

695695
/*******************************************************************\
696696
697-
Function: expr2verilogt::convert_explicit_cast
697+
Function: expr2verilogt::convert_explicit_const_cast
698698
699699
Inputs:
700700
@@ -704,8 +704,47 @@ Function: expr2verilogt::convert_explicit_cast
704704
705705
\*******************************************************************/
706706

707-
expr2verilogt::resultt
708-
expr2verilogt::convert_explicit_cast(const verilog_explicit_cast_exprt &src)
707+
expr2verilogt::resultt expr2verilogt::convert_explicit_const_cast(
708+
const verilog_explicit_const_cast_exprt &src)
709+
{
710+
return {verilog_precedencet::MAX, "const'(" + convert_rec(src.op()).s + ')'};
711+
}
712+
713+
/*******************************************************************\
714+
715+
Function: expr2verilogt::convert_explicit_signing_cast
716+
717+
Inputs:
718+
719+
Outputs:
720+
721+
Purpose:
722+
723+
\*******************************************************************/
724+
725+
expr2verilogt::resultt expr2verilogt::convert_explicit_signing_cast(
726+
const verilog_explicit_signing_cast_exprt &src)
727+
{
728+
std::string signing = src.is_signed() ? "signed" : "unsigned";
729+
730+
return {
731+
verilog_precedencet::MAX, signing + "'(" + convert_rec(src.op()).s + ')'};
732+
}
733+
734+
/*******************************************************************\
735+
736+
Function: expr2verilogt::convert_explicit_type_cast
737+
738+
Inputs:
739+
740+
Outputs:
741+
742+
Purpose:
743+
744+
\*******************************************************************/
745+
746+
expr2verilogt::resultt expr2verilogt::convert_explicit_type_cast(
747+
const verilog_explicit_type_cast_exprt &src)
709748
{
710749
return {
711750
verilog_precedencet::MAX,
@@ -714,7 +753,7 @@ expr2verilogt::convert_explicit_cast(const verilog_explicit_cast_exprt &src)
714753

715754
/*******************************************************************\
716755
717-
Function: expr2verilogt::convert_size_cast
756+
Function: expr2verilogt::convert_explicit_size_cast
718757
719758
Inputs:
720759
@@ -724,8 +763,8 @@ Function: expr2verilogt::convert_size_cast
724763
725764
\*******************************************************************/
726765

727-
expr2verilogt::resultt
728-
expr2verilogt::convert_size_cast(const verilog_size_cast_exprt &src)
766+
expr2verilogt::resultt expr2verilogt::convert_explicit_size_cast(
767+
const verilog_explicit_size_cast_exprt &src)
729768
{
730769
return {
731770
verilog_precedencet::MAX,
@@ -1490,11 +1529,19 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
14901529
return convert_unary(
14911530
to_bitnot_expr(src), "~", precedence = verilog_precedencet::NOT);
14921531

1493-
else if(src.id() == ID_verilog_explicit_cast)
1494-
return convert_explicit_cast(to_verilog_explicit_cast_expr(src));
1532+
else if(src.id() == ID_verilog_explicit_const_cast)
1533+
return convert_explicit_const_cast(
1534+
to_verilog_explicit_const_cast_expr(src));
1535+
1536+
else if(src.id() == ID_verilog_explicit_size_cast)
1537+
return convert_explicit_size_cast(to_verilog_explicit_size_cast_expr(src));
1538+
1539+
else if(src.id() == ID_verilog_explicit_signing_cast)
1540+
return convert_explicit_signing_cast(
1541+
to_verilog_explicit_signing_cast_expr(src));
14951542

1496-
else if(src.id() == ID_verilog_size_cast)
1497-
return convert_size_cast(to_verilog_size_cast_expr(src));
1543+
else if(src.id() == ID_verilog_explicit_type_cast)
1544+
return convert_explicit_type_cast(to_verilog_explicit_type_cast_expr(src));
14981545

14991546
else if(src.id()==ID_typecast)
15001547
return convert_typecast(to_typecast_expr(src));

‎src/verilog/expr2verilog_class.h‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -105,11 +105,19 @@ class expr2verilogt
105105

106106
resultt convert_constant(const constant_exprt &, verilog_precedencet &);
107107

108-
resultt convert_explicit_cast(const class verilog_explicit_cast_exprt &);
108+
resultt
109+
convert_explicit_const_cast(const class verilog_explicit_const_cast_exprt &);
110+
111+
resultt convert_explicit_signing_cast(
112+
const class verilog_explicit_signing_cast_exprt &);
113+
114+
resultt
115+
convert_explicit_type_cast(const class verilog_explicit_type_cast_exprt &);
109116

110117
resultt convert_typecast(const typecast_exprt &);
111118

112-
resultt convert_size_cast(const class verilog_size_cast_exprt &);
119+
resultt
120+
convert_explicit_size_cast(const class verilog_explicit_size_cast_exprt &);
113121

114122
resultt
115123
convert_concatenation(const concatenation_exprt &, verilog_precedencet);

‎src/verilog/parser.y‎

Lines changed: 18 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1419,11 +1419,27 @@ lifetime:
14191419

14201420
casting_type:
14211421
simple_type
1422+
{
1423+
init($$, ID_verilog_explicit_type_cast);
1424+
stack_expr($$).type() = stack_type($1);
1425+
}
14221426
| constant_primary
1423-
{ init($$, ID_verilog_size_cast); mto($$, $1); }
1427+
{ init($$, ID_verilog_explicit_size_cast); mto($$, $1); }
14241428
| signing
1429+
{
1430+
init($$, ID_verilog_explicit_signing_cast);
1431+
stack_expr($$).type() = stack_type($1);
1432+
}
14251433
| TOK_STRING
1434+
{
1435+
init($$, ID_verilog_explicit_type_cast);
1436+
stack_expr($$).type() = stack_type($1);
1437+
}
14261438
| TOK_CONST
1439+
{
1440+
init($$, ID_verilog_explicit_const_cast);
1441+
stack_expr($$).type() = stack_type($1);
1442+
}
14271443
;
14281444

14291445
data_type:
@@ -4044,18 +4060,7 @@ time_literal: TOK_TIME_LITERAL
40444060

40454061
cast:
40464062
casting_type '\'' '(' expression ')'
4047-
{ if(stack_expr($1).id() == ID_verilog_size_cast)
4048-
{
4049-
$$ = $1;
4050-
mto($$, $4);
4051-
}
4052-
else
4053-
{
4054-
init($$, ID_verilog_explicit_cast);
4055-
stack_expr($$).type() = stack_type($1);
4056-
mto($$, $4);
4057-
}
4058-
}
4063+
{ $$ = $1; mto($$, $4); }
40594064
;
40604065

40614066
// System Verilog standard 1800-2017

‎src/verilog/verilog_expr.h‎

Lines changed: 94 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -2462,13 +2462,13 @@ inline verilog_udpt &to_verilog_udp(irept &irep)
24622462
}
24632463

24642464
/// size'(expression)
2465-
class verilog_size_cast_exprt : public binary_exprt
2465+
class verilog_explicit_size_cast_exprt : public binary_exprt
24662466
{
24672467
public:
2468-
verilog_size_cast_exprt(exprt __size, exprt __op, typet __type)
2468+
verilog_explicit_size_cast_exprt(exprt __size, exprt __op, typet __type)
24692469
: binary_exprt(
24702470
std::move(__size),
2471-
ID_verilog_size_cast,
2471+
ID_verilog_explicit_size_cast,
24722472
std::move(__op),
24732473
std::move(__type))
24742474
{
@@ -2501,24 +2501,97 @@ class verilog_size_cast_exprt : public binary_exprt
25012501
}
25022502
};
25032503

2504-
inline const verilog_size_cast_exprt &
2505-
to_verilog_size_cast_expr(const exprt &expr)
2504+
inline const verilog_explicit_size_cast_exprt &
2505+
to_verilog_explicit_size_cast_expr(const exprt &expr)
25062506
{
2507-
verilog_size_cast_exprt::check(expr);
2508-
return static_cast<const verilog_size_cast_exprt &>(expr);
2507+
verilog_explicit_size_cast_exprt::check(expr);
2508+
return static_cast<const verilog_explicit_size_cast_exprt &>(expr);
25092509
}
25102510

2511-
inline verilog_size_cast_exprt &to_verilog_size_cast_expr(exprt &expr)
2511+
inline verilog_explicit_size_cast_exprt &
2512+
to_verilog_explicit_size_cast_expr(exprt &expr)
25122513
{
2513-
verilog_size_cast_exprt::check(expr);
2514-
return static_cast<verilog_size_cast_exprt &>(expr);
2514+
verilog_explicit_size_cast_exprt::check(expr);
2515+
return static_cast<verilog_explicit_size_cast_exprt &>(expr);
25152516
}
25162517

2517-
class verilog_explicit_cast_exprt : public unary_exprt
2518+
class verilog_explicit_const_cast_exprt : public unary_exprt
25182519
{
25192520
public:
2520-
verilog_explicit_cast_exprt(exprt __op, typet __type)
2521-
: unary_exprt(ID_verilog_explicit_cast, std::move(__op), std::move(__type))
2521+
verilog_explicit_const_cast_exprt(exprt __op, typet __type)
2522+
: unary_exprt(
2523+
ID_verilog_explicit_const_cast,
2524+
std::move(__op),
2525+
std::move(__type))
2526+
{
2527+
}
2528+
2529+
exprt lower() const
2530+
{
2531+
return typecast_exprt{op(), type()};
2532+
}
2533+
};
2534+
2535+
inline const verilog_explicit_const_cast_exprt &
2536+
to_verilog_explicit_const_cast_expr(const exprt &expr)
2537+
{
2538+
verilog_explicit_const_cast_exprt::check(expr);
2539+
return static_cast<const verilog_explicit_const_cast_exprt &>(expr);
2540+
}
2541+
2542+
inline verilog_explicit_const_cast_exprt &
2543+
to_verilog_explicit_const_cast_expr(exprt &expr)
2544+
{
2545+
verilog_explicit_const_cast_exprt::check(expr);
2546+
return static_cast<verilog_explicit_const_cast_exprt &>(expr);
2547+
}
2548+
2549+
class verilog_explicit_signing_cast_exprt : public unary_exprt
2550+
{
2551+
public:
2552+
verilog_explicit_signing_cast_exprt(exprt __op, typet __type)
2553+
: unary_exprt(
2554+
ID_verilog_explicit_signing_cast,
2555+
std::move(__op),
2556+
std::move(__type))
2557+
{
2558+
}
2559+
2560+
bool is_signed() const
2561+
{
2562+
auto &dest_type = type();
2563+
return dest_type.id() == ID_signedbv ||
2564+
dest_type.id() == ID_verilog_signedbv;
2565+
}
2566+
2567+
exprt lower() const
2568+
{
2569+
return typecast_exprt{op(), type()};
2570+
}
2571+
};
2572+
2573+
inline const verilog_explicit_signing_cast_exprt &
2574+
to_verilog_explicit_signing_cast_expr(const exprt &expr)
2575+
{
2576+
verilog_explicit_signing_cast_exprt::check(expr);
2577+
return static_cast<const verilog_explicit_signing_cast_exprt &>(expr);
2578+
}
2579+
2580+
inline verilog_explicit_signing_cast_exprt &
2581+
to_verilog_explicit_signing_cast_expr(exprt &expr)
2582+
{
2583+
verilog_explicit_signing_cast_exprt::check(expr);
2584+
return static_cast<verilog_explicit_signing_cast_exprt &>(expr);
2585+
}
2586+
2587+
class verilog_explicit_type_cast_exprt : public unary_exprt
2588+
{
2589+
public:
2590+
verilog_explicit_type_cast_exprt(exprt __op, typet __type)
2591+
: unary_exprt(
2592+
ID_verilog_explicit_type_cast,
2593+
std::move(__op),
2594+
std::move(__type))
25222595
{
25232596
}
25242597

@@ -2528,17 +2601,18 @@ class verilog_explicit_cast_exprt : public unary_exprt
25282601
}
25292602
};
25302603

2531-
inline const verilog_explicit_cast_exprt &
2532-
to_verilog_explicit_cast_expr(const exprt &expr)
2604+
inline const verilog_explicit_type_cast_exprt &
2605+
to_verilog_explicit_type_cast_expr(const exprt &expr)
25332606
{
2534-
verilog_explicit_cast_exprt::check(expr);
2535-
return static_cast<const verilog_explicit_cast_exprt &>(expr);
2607+
verilog_explicit_type_cast_exprt::check(expr);
2608+
return static_cast<const verilog_explicit_type_cast_exprt &>(expr);
25362609
}
25372610

2538-
inline verilog_explicit_cast_exprt &to_verilog_explicit_cast_expr(exprt &expr)
2611+
inline verilog_explicit_type_cast_exprt &
2612+
to_verilog_explicit_type_cast_expr(exprt &expr)
25392613
{
2540-
verilog_explicit_cast_exprt::check(expr);
2541-
return static_cast<verilog_explicit_cast_exprt &>(expr);
2614+
verilog_explicit_type_cast_exprt::check(expr);
2615+
return static_cast<verilog_explicit_type_cast_exprt &>(expr);
25422616
}
25432617

25442618
class verilog_implicit_typecast_exprt : public unary_exprt

‎src/verilog/verilog_lowering.cpp‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -274,13 +274,17 @@ exprt verilog_lowering(exprt expr)
274274

275275
return expr;
276276
}
277-
else if(expr.id() == ID_verilog_explicit_cast)
277+
else if(expr.id() == ID_verilog_explicit_type_cast)
278278
{
279-
return to_verilog_explicit_cast_expr(expr).lower();
279+
return to_verilog_explicit_type_cast_expr(expr).lower();
280280
}
281-
else if(expr.id() == ID_verilog_size_cast)
281+
else if(expr.id() == ID_verilog_explicit_signing_cast)
282282
{
283-
return to_verilog_size_cast_expr(expr).lower();
283+
return to_verilog_explicit_signing_cast_expr(expr).lower();
284+
}
285+
else if(expr.id() == ID_verilog_explicit_size_cast)
286+
{
287+
return to_verilog_explicit_size_cast_expr(expr).lower();
284288
}
285289
else if(
286290
expr.id() == ID_verilog_streaming_concatenation_left_to_right ||

0 commit comments

Comments
 (0)