@@ -44,6 +44,94 @@ Author: Daniel Kroening, kroening@kroening.com
4444
4545#include < sstream>
4646
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+
47135void c_typecheck_baset::typecheck_expr (exprt &expr)
48136{
49137 if (expr.id ()==ID_already_typechecked)
@@ -4527,94 +4615,6 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
45274615 throw 0 ;
45284616}
45294617
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-
46184618void c_typecheck_baset::make_constant (exprt &expr)
46194619{
46204620 // Floating-point expressions may require a rounding mode.
0 commit comments