@@ -44,6 +44,94 @@ Author: Daniel Kroening, kroening@kroening.com
44
44
45
45
#include < sstream>
46
46
47
+ // / Architecturally similar to \ref can_forward_propagatet, but specialized for
48
+ // / what is a constexpr, i.e., an expression that can be fully evaluated at
49
+ // / compile time.
50
+ class is_compile_time_constantt
51
+ {
52
+ public:
53
+ explicit is_compile_time_constantt (const namespacet &ns) : ns(ns)
54
+ {
55
+ }
56
+
57
+ // / returns true iff the expression can be considered constant
58
+ bool operator ()(const exprt &e) const
59
+ {
60
+ return is_constant (e);
61
+ }
62
+
63
+ protected:
64
+ const namespacet &ns;
65
+
66
+ // / This function determines what expressions are to be propagated as
67
+ // / "constants"
68
+ bool is_constant (const exprt &e) const
69
+ {
70
+ if (e.id () == ID_infinity)
71
+ return true ;
72
+
73
+ if (e.is_constant ())
74
+ return true ;
75
+
76
+ if (e.id () == ID_address_of)
77
+ {
78
+ return is_constant_address_of (to_address_of_expr (e).object ());
79
+ }
80
+ else if (
81
+ e.id () == ID_typecast || e.id () == ID_array_of || e.id () == ID_plus ||
82
+ e.id () == ID_mult || e.id () == ID_array || e.id () == ID_with ||
83
+ e.id () == ID_struct || e.id () == ID_union || e.id () == ID_empty_union ||
84
+ e.id () == ID_equal || e.id () == ID_notequal || e.id () == ID_lt ||
85
+ e.id () == ID_le || e.id () == ID_gt || e.id () == ID_ge ||
86
+ e.id () == ID_if || e.id () == ID_not || e.id () == ID_and ||
87
+ e.id () == ID_or || e.id () == ID_bitnot || e.id () == ID_bitand ||
88
+ e.id () == ID_bitor || e.id () == ID_bitxor || e.id () == ID_vector)
89
+ {
90
+ return std::all_of (
91
+ e.operands ().begin (), e.operands ().end (), [this ](const exprt &op) {
92
+ return is_constant (op);
93
+ });
94
+ }
95
+
96
+ return false ;
97
+ }
98
+
99
+ // / this function determines which reference-typed expressions are constant
100
+ bool is_constant_address_of (const exprt &e) const
101
+ {
102
+ if (e.id () == ID_symbol)
103
+ {
104
+ return e.type ().id () == ID_code ||
105
+ ns.lookup (to_symbol_expr (e).get_identifier ()).is_static_lifetime ;
106
+ }
107
+ else if (e.id () == ID_array && e.get_bool (ID_C_string_constant))
108
+ return true ;
109
+ else if (e.id () == ID_label)
110
+ return true ;
111
+ else if (e.id () == ID_index)
112
+ {
113
+ const index_exprt &index_expr = to_index_expr (e);
114
+
115
+ return is_constant_address_of (index_expr.array ()) &&
116
+ is_constant (index_expr.index ());
117
+ }
118
+ else if (e.id () == ID_member)
119
+ {
120
+ return is_constant_address_of (to_member_expr (e).compound ());
121
+ }
122
+ else if (e.id () == ID_dereference)
123
+ {
124
+ const dereference_exprt &deref = to_dereference_expr (e);
125
+
126
+ return is_constant (deref.pointer ());
127
+ }
128
+ else if (e.id () == ID_string_constant)
129
+ return true ;
130
+
131
+ return false ;
132
+ }
133
+ };
134
+
47
135
void c_typecheck_baset::typecheck_expr (exprt &expr)
48
136
{
49
137
if (expr.id ()==ID_already_typechecked)
@@ -4527,94 +4615,6 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
4527
4615
throw 0 ;
4528
4616
}
4529
4617
4530
- // / Architecturally similar to \ref can_forward_propagatet, but specialized for
4531
- // / what is a constexpr, i.e., an expression that can be fully evaluated at
4532
- // / compile time.
4533
- class is_compile_time_constantt
4534
- {
4535
- public:
4536
- explicit is_compile_time_constantt (const namespacet &ns) : ns(ns)
4537
- {
4538
- }
4539
-
4540
- // / returns true iff the expression can be considered constant
4541
- bool operator ()(const exprt &e) const
4542
- {
4543
- return is_constant (e);
4544
- }
4545
-
4546
- protected:
4547
- const namespacet &ns;
4548
-
4549
- // / This function determines what expressions are to be propagated as
4550
- // / "constants"
4551
- bool is_constant (const exprt &e) const
4552
- {
4553
- if (e.id () == ID_infinity)
4554
- return true ;
4555
-
4556
- if (e.is_constant ())
4557
- return true ;
4558
-
4559
- if (e.id () == ID_address_of)
4560
- {
4561
- return is_constant_address_of (to_address_of_expr (e).object ());
4562
- }
4563
- else if (
4564
- e.id () == ID_typecast || e.id () == ID_array_of || e.id () == ID_plus ||
4565
- e.id () == ID_mult || e.id () == ID_array || e.id () == ID_with ||
4566
- e.id () == ID_struct || e.id () == ID_union || e.id () == ID_empty_union ||
4567
- e.id () == ID_equal || e.id () == ID_notequal || e.id () == ID_lt ||
4568
- e.id () == ID_le || e.id () == ID_gt || e.id () == ID_ge ||
4569
- e.id () == ID_if || e.id () == ID_not || e.id () == ID_and ||
4570
- e.id () == ID_or || e.id () == ID_bitnot || e.id () == ID_bitand ||
4571
- e.id () == ID_bitor || e.id () == ID_bitxor || e.id () == ID_vector)
4572
- {
4573
- return std::all_of (
4574
- e.operands ().begin (), e.operands ().end (), [this ](const exprt &op) {
4575
- return is_constant (op);
4576
- });
4577
- }
4578
-
4579
- return false ;
4580
- }
4581
-
4582
- // / this function determines which reference-typed expressions are constant
4583
- bool is_constant_address_of (const exprt &e) const
4584
- {
4585
- if (e.id () == ID_symbol)
4586
- {
4587
- return e.type ().id () == ID_code ||
4588
- ns.lookup (to_symbol_expr (e).get_identifier ()).is_static_lifetime ;
4589
- }
4590
- else if (e.id () == ID_array && e.get_bool (ID_C_string_constant))
4591
- return true ;
4592
- else if (e.id () == ID_label)
4593
- return true ;
4594
- else if (e.id () == ID_index)
4595
- {
4596
- const index_exprt &index_expr = to_index_expr (e);
4597
-
4598
- return is_constant_address_of (index_expr.array ()) &&
4599
- is_constant (index_expr.index ());
4600
- }
4601
- else if (e.id () == ID_member)
4602
- {
4603
- return is_constant_address_of (to_member_expr (e).compound ());
4604
- }
4605
- else if (e.id () == ID_dereference)
4606
- {
4607
- const dereference_exprt &deref = to_dereference_expr (e);
4608
-
4609
- return is_constant (deref.pointer ());
4610
- }
4611
- else if (e.id () == ID_string_constant)
4612
- return true ;
4613
-
4614
- return false ;
4615
- }
4616
- };
4617
-
4618
4618
void c_typecheck_baset::make_constant (exprt &expr)
4619
4619
{
4620
4620
// Floating-point expressions may require a rounding mode.
0 commit comments