@@ -43,6 +43,94 @@ Author: Daniel Kroening, kroening@kroening.com
4343
4444#include < sstream>
4545
46+ // / Architecturally similar to \ref can_forward_propagatet, but specialized for
47+ // / what is a constexpr, i.e., an expression that can be fully evaluated at
48+ // / compile time.
49+ class is_compile_time_constantt
50+ {
51+ public:
52+ explicit is_compile_time_constantt (const namespacet &ns) : ns(ns)
53+ {
54+ }
55+
56+ // / returns true iff the expression can be considered constant
57+ bool operator ()(const exprt &e) const
58+ {
59+ return is_constant (e);
60+ }
61+
62+ protected:
63+ const namespacet &ns;
64+
65+ // / This function determines what expressions are to be propagated as
66+ // / "constants"
67+ bool is_constant (const exprt &e) const
68+ {
69+ if (e.id () == ID_infinity)
70+ return true ;
71+
72+ if (e.is_constant ())
73+ return true ;
74+
75+ if (e.id () == ID_address_of)
76+ {
77+ return is_constant_address_of (to_address_of_expr (e).object ());
78+ }
79+ else if (
80+ e.id () == ID_typecast || e.id () == ID_array_of || e.id () == ID_plus ||
81+ e.id () == ID_mult || e.id () == ID_array || e.id () == ID_with ||
82+ e.id () == ID_struct || e.id () == ID_union || e.id () == ID_empty_union ||
83+ e.id () == ID_equal || e.id () == ID_notequal || e.id () == ID_lt ||
84+ e.id () == ID_le || e.id () == ID_gt || e.id () == ID_ge ||
85+ e.id () == ID_if || e.id () == ID_not || e.id () == ID_and ||
86+ e.id () == ID_or || e.id () == ID_bitnot || e.id () == ID_bitand ||
87+ e.id () == ID_bitor || e.id () == ID_bitxor || e.id () == ID_vector)
88+ {
89+ return std::all_of (
90+ e.operands ().begin (),
91+ e.operands ().end (),
92+ [this ](const exprt &op) { return is_constant (op); });
93+ }
94+
95+ return false ;
96+ }
97+
98+ // / this function determines which reference-typed expressions are constant
99+ bool is_constant_address_of (const exprt &e) const
100+ {
101+ if (e.id () == ID_symbol)
102+ {
103+ return e.type ().id () == ID_code ||
104+ ns.lookup (to_symbol_expr (e).get_identifier ()).is_static_lifetime ;
105+ }
106+ else if (e.id () == ID_array && e.get_bool (ID_C_string_constant))
107+ return true ;
108+ else if (e.id () == ID_label)
109+ return true ;
110+ else if (e.id () == ID_index)
111+ {
112+ const index_exprt &index_expr = to_index_expr (e);
113+
114+ return is_constant_address_of (index_expr.array ()) &&
115+ is_constant (index_expr.index ());
116+ }
117+ else if (e.id () == ID_member)
118+ {
119+ return is_constant_address_of (to_member_expr (e).compound ());
120+ }
121+ else if (e.id () == ID_dereference)
122+ {
123+ const dereference_exprt &deref = to_dereference_expr (e);
124+
125+ return is_constant (deref.pointer ());
126+ }
127+ else if (e.id () == ID_string_constant)
128+ return true ;
129+
130+ return false ;
131+ }
132+ };
133+
46134void c_typecheck_baset::typecheck_expr (exprt &expr)
47135{
48136 if (expr.id ()==ID_already_typechecked)
@@ -4666,94 +4754,6 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
46664754 throw 0 ;
46674755}
46684756
4669- // / Architecturally similar to \ref can_forward_propagatet, but specialized for
4670- // / what is a constexpr, i.e., an expression that can be fully evaluated at
4671- // / compile time.
4672- class is_compile_time_constantt
4673- {
4674- public:
4675- explicit is_compile_time_constantt (const namespacet &ns) : ns(ns)
4676- {
4677- }
4678-
4679- // / returns true iff the expression can be considered constant
4680- bool operator ()(const exprt &e) const
4681- {
4682- return is_constant (e);
4683- }
4684-
4685- protected:
4686- const namespacet &ns;
4687-
4688- // / This function determines what expressions are to be propagated as
4689- // / "constants"
4690- bool is_constant (const exprt &e) const
4691- {
4692- if (e.id () == ID_infinity)
4693- return true ;
4694-
4695- if (e.is_constant ())
4696- return true ;
4697-
4698- if (e.id () == ID_address_of)
4699- {
4700- return is_constant_address_of (to_address_of_expr (e).object ());
4701- }
4702- else if (
4703- e.id () == ID_typecast || e.id () == ID_array_of || e.id () == ID_plus ||
4704- e.id () == ID_mult || e.id () == ID_array || e.id () == ID_with ||
4705- e.id () == ID_struct || e.id () == ID_union || e.id () == ID_empty_union ||
4706- e.id () == ID_equal || e.id () == ID_notequal || e.id () == ID_lt ||
4707- e.id () == ID_le || e.id () == ID_gt || e.id () == ID_ge ||
4708- e.id () == ID_if || e.id () == ID_not || e.id () == ID_and ||
4709- e.id () == ID_or || e.id () == ID_bitnot || e.id () == ID_bitand ||
4710- e.id () == ID_bitor || e.id () == ID_bitxor || e.id () == ID_vector)
4711- {
4712- return std::all_of (
4713- e.operands ().begin (), e.operands ().end (), [this ](const exprt &op) {
4714- return is_constant (op);
4715- });
4716- }
4717-
4718- return false ;
4719- }
4720-
4721- // / this function determines which reference-typed expressions are constant
4722- bool is_constant_address_of (const exprt &e) const
4723- {
4724- if (e.id () == ID_symbol)
4725- {
4726- return e.type ().id () == ID_code ||
4727- ns.lookup (to_symbol_expr (e).get_identifier ()).is_static_lifetime ;
4728- }
4729- else if (e.id () == ID_array && e.get_bool (ID_C_string_constant))
4730- return true ;
4731- else if (e.id () == ID_label)
4732- return true ;
4733- else if (e.id () == ID_index)
4734- {
4735- const index_exprt &index_expr = to_index_expr (e);
4736-
4737- return is_constant_address_of (index_expr.array ()) &&
4738- is_constant (index_expr.index ());
4739- }
4740- else if (e.id () == ID_member)
4741- {
4742- return is_constant_address_of (to_member_expr (e).compound ());
4743- }
4744- else if (e.id () == ID_dereference)
4745- {
4746- const dereference_exprt &deref = to_dereference_expr (e);
4747-
4748- return is_constant (deref.pointer ());
4749- }
4750- else if (e.id () == ID_string_constant)
4751- return true ;
4752-
4753- return false ;
4754- }
4755- };
4756-
47574757void c_typecheck_baset::make_constant (exprt &expr)
47584758{
47594759 source_locationt location = expr.find_source_location ();
0 commit comments