@@ -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)
@@ -4561,94 +4649,6 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
45614649 throw 0 ;
45624650}
45634651
4564- // / Architecturally similar to \ref can_forward_propagatet, but specialized for
4565- // / what is a constexpr, i.e., an expression that can be fully evaluated at
4566- // / compile time.
4567- class is_compile_time_constantt
4568- {
4569- public:
4570- explicit is_compile_time_constantt (const namespacet &ns) : ns(ns)
4571- {
4572- }
4573-
4574- // / returns true iff the expression can be considered constant
4575- bool operator ()(const exprt &e) const
4576- {
4577- return is_constant (e);
4578- }
4579-
4580- protected:
4581- const namespacet &ns;
4582-
4583- // / This function determines what expressions are to be propagated as
4584- // / "constants"
4585- bool is_constant (const exprt &e) const
4586- {
4587- if (e.id () == ID_infinity)
4588- return true ;
4589-
4590- if (e.is_constant ())
4591- return true ;
4592-
4593- if (e.id () == ID_address_of)
4594- {
4595- return is_constant_address_of (to_address_of_expr (e).object ());
4596- }
4597- else if (
4598- e.id () == ID_typecast || e.id () == ID_array_of || e.id () == ID_plus ||
4599- e.id () == ID_mult || e.id () == ID_array || e.id () == ID_with ||
4600- e.id () == ID_struct || e.id () == ID_union || e.id () == ID_empty_union ||
4601- e.id () == ID_equal || e.id () == ID_notequal || e.id () == ID_lt ||
4602- e.id () == ID_le || e.id () == ID_gt || e.id () == ID_ge ||
4603- e.id () == ID_if || e.id () == ID_not || e.id () == ID_and ||
4604- e.id () == ID_or || e.id () == ID_bitnot || e.id () == ID_bitand ||
4605- e.id () == ID_bitor || e.id () == ID_bitxor || e.id () == ID_vector)
4606- {
4607- return std::all_of (
4608- e.operands ().begin (), e.operands ().end (), [this ](const exprt &op) {
4609- return is_constant (op);
4610- });
4611- }
4612-
4613- return false ;
4614- }
4615-
4616- // / this function determines which reference-typed expressions are constant
4617- bool is_constant_address_of (const exprt &e) const
4618- {
4619- if (e.id () == ID_symbol)
4620- {
4621- return e.type ().id () == ID_code ||
4622- ns.lookup (to_symbol_expr (e).get_identifier ()).is_static_lifetime ;
4623- }
4624- else if (e.id () == ID_array && e.get_bool (ID_C_string_constant))
4625- return true ;
4626- else if (e.id () == ID_label)
4627- return true ;
4628- else if (e.id () == ID_index)
4629- {
4630- const index_exprt &index_expr = to_index_expr (e);
4631-
4632- return is_constant_address_of (index_expr.array ()) &&
4633- is_constant (index_expr.index ());
4634- }
4635- else if (e.id () == ID_member)
4636- {
4637- return is_constant_address_of (to_member_expr (e).compound ());
4638- }
4639- else if (e.id () == ID_dereference)
4640- {
4641- const dereference_exprt &deref = to_dereference_expr (e);
4642-
4643- return is_constant (deref.pointer ());
4644- }
4645- else if (e.id () == ID_string_constant)
4646- return true ;
4647-
4648- return false ;
4649- }
4650- };
4651-
46524652void c_typecheck_baset::make_constant (exprt &expr)
46534653{
46544654 // Floating-point expressions may require a rounding mode.
0 commit comments