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.

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