aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Ceval.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2018-04-26 18:00:36 +0200
committerGitHub <noreply@github.com>2018-04-26 18:00:36 +0200
commitf1d9a90486ac2744e0f2096eeaeedac117af5b9a (patch)
tree17da3fcddc04d9710f245a64e6124d7d13807c6a /cparser/Ceval.ml
parent7d91167706b72103ddf9f4088cf02dd9761fdf47 (diff)
downloadcompcert-kvx-f1d9a90486ac2744e0f2096eeaeedac117af5b9a.tar.gz
compcert-kvx-f1d9a90486ac2744e0f2096eeaeedac117af5b9a.zip
Earlier, more comprehensive check for constant initializers (#88)
This commit checks *during elaboration* that initializers for global variables or local static variables are compile-time constants. Before this commit, some non-constant initializers were detected later in the C2C pass, but others were eliminated by the Cleanup pass before being checked, and yet others could cause the Rename pass to abort. To determine which variables are constant l-values, we leverage the recent addition of the Storage_auto storage class and base the determination on the storage class of the identifier: 'auto' or 'register' is not constant, the others are constant.
Diffstat (limited to 'cparser/Ceval.ml')
-rw-r--r--cparser/Ceval.ml92
1 files changed, 91 insertions, 1 deletions
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index c3d7eeeb..f479ad5c 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -13,7 +13,7 @@
(* *)
(* *********************************************************************)
-(* Evaluation of compile-time constants *)
+(* Evaluation and recognition of compile-time constants *)
open C
open Cutil
@@ -279,3 +279,93 @@ let constant_expr env ty e =
| TEnum(_, _), I n -> Some(CInt(n, enum_ikind, ""))
| _ -> None
with Notconst -> None
+
+(* Recognition of constant initializers and constant expressions.
+ This is just a check: no evaluation of the constants is done.
+ Reference: ISO C99 section 6.6 *)
+
+let rec is_constant_init env = function
+ | Init_single e -> is_constant_expr env e
+ | Init_array il -> List.for_all (is_constant_init env) il
+ | Init_struct(id, fil) ->
+ List.for_all (fun (f, i) -> is_constant_init env i) fil
+ | Init_union(id, f, i) -> is_constant_init env i
+
+and is_constant_expr env e =
+ match e.edesc with
+ | EConst cst -> true
+ | ESizeof ty -> true
+ | EAlignof ty -> true
+ | EVar id ->
+ begin match Env.find_ident env id with
+ | Env.II_ident _ -> is_constant_rval_of_lval env e
+ | Env.II_enum _ -> true (* an enum value is a constant *)
+ | exception Env.Error _ -> false (* should not happen *)
+ end
+ | EUnop(op, e1) ->
+ begin match op with
+ | Ominus | Oplus | Olognot | Onot -> is_constant_expr env e1
+ | Oderef | Odot _ | Oarrow _ -> is_constant_rval_of_lval env e
+ | Oaddrof -> is_constant_lval env e1
+ | Opreincr | Opredecr | Opostincr | Opostdecr -> false
+ (* Constant expressions shall not contain increment or decrement *)
+ end
+ | EBinop(op, e1, e2, _) ->
+ begin match op with
+ | Oadd | Osub | Omul | Odiv | Omod
+ | Oand | Oor | Oxor | Oshl | Oshr
+ | Oeq | One | Olt | Ogt | Ole | Oge
+ | Ocomma | Ologand | Ologor ->
+ is_constant_expr env e1 && is_constant_expr env e2
+ (* ISO C99 says that constant expressions shall not contain comma
+ operators. However, clang accepts them, and they are harmless. *)
+ | Oindex ->
+ is_constant_rval_of_lval env e
+ | Oassign
+ | Oadd_assign | Osub_assign | Omul_assign | Odiv_assign | Omod_assign
+ | Oand_assign | Oor_assign | Oxor_assign | Oshl_assign | Oshr_assign ->
+ false
+ (* constant expressions shall not contain assignments *)
+ end
+ | EConditional(e1, e2, e3) ->
+ is_constant_expr env e1 && is_constant_expr env e2
+ && is_constant_expr env e3
+ | ECast(ty, e1) ->
+ is_constant_expr env e1
+ | ECompound(ty, i) ->
+ is_constant_init env i
+ | ECall(fn, args) ->
+ false
+ (* constant expressions shall not contain function calls *)
+
+and is_constant_rval_of_lval env e =
+ (* The value of an object shall not be accessed by use of the . -> * []
+ operators. This is the case if the object has array or function type.
+ A scalar type or a composite type implies a memory access. *)
+ match unroll env e.etyp with
+ | TArray _ | TFun _ -> is_constant_lval env e
+ | _ -> false
+
+and is_constant_lval env e =
+ match e.edesc with
+ | EVar id ->
+ begin match Env.find_ident env id with
+ | Env.II_ident(sto, _) ->
+ begin match sto with
+ | Storage_default | Storage_extern | Storage_static -> true
+ | Storage_auto | Storage_register -> false
+ end
+ | Env.II_enum _ -> false (* should not happen *)
+ | exception Env.Error _ -> false (* should not happen *)
+ end
+ | EUnop(Oderef, e1) -> is_constant_expr env e1
+ | EUnop(Odot f, e1) -> is_constant_lval env e1
+ | EUnop(Oarrow f, e1) -> is_constant_expr env e1
+ | EBinop(Oindex, e1, e2, _) ->
+ is_constant_expr env e1 && is_constant_expr env e2
+ | ECompound(ty, i) ->
+ is_constant_init env i
+ | _ -> false
+
+
+