diff options
| -rw-r--r-- | cparser/Ceval.ml | 92 | ||||
| -rw-r--r-- | cparser/Ceval.mli | 2 | ||||
| -rw-r--r-- | cparser/Elab.ml | 9 |
3 files changed, 99 insertions, 4 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 + + + diff --git a/cparser/Ceval.mli b/cparser/Ceval.mli index 7425a332..32a0ed91 100644 --- a/cparser/Ceval.mli +++ b/cparser/Ceval.mli @@ -16,3 +16,5 @@ val integer_expr : Env.t -> C.exp -> int64 option val constant_expr : Env.t -> C.typ -> C.exp -> C.constant option val normalize_int : int64 -> C.ikind -> int64 +val is_constant_init: Env.t -> C.init -> bool +val is_constant_expr: Env.t -> C.exp -> bool diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 55764c3c..dddbd03b 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2236,9 +2236,6 @@ let enter_decdefs local loc env sto dl = fatal_error loc "'%s' has incomplete type" s; (* process the initializer *) let (ty', init') = elab_initializer loc env1 s ty init in - (* if (sto = Storage_static || not local) then - * (\* Check for constant initializer for static and global variables *\) - * is_constant_init env loc init'; *) (* update environment with refined type *) let env2 = Env.add_ident env1 id sto' ty' in (* check for incomplete type *) @@ -2252,6 +2249,12 @@ let enter_decdefs local loc env sto dl = else begin (* Global definition *) emit_elab ~linkage env2 loc (Gdecl(sto', id, ty', init')); + (* Make sure the initializer is constant. *) + begin match init' with + | Some i when not (Ceval.is_constant_init env2 i) -> + error loc "initializer is not a compile-time constant" + | _ -> () + end; (decls, env2) end in let (decls, env') = List.fold_left enter_decdef ([], env) dl in |