Initializers: handle By_copy accesses (e.g. for &(glob.field))

C2C: insert the correct Evalof for structs; clean up unused memcpy stuff
test/regression: run with interpreter
test/regression: add test cas &(glob.field) to initializers.c


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1815 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 8 insertions, 47 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index d4faa2b..a5a9fee 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -74,14 +74,6 @@ let builtins_generic = {
     (* Floating-point absolute value *)
     "__builtin_fabs",
       (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
-    (* Block copy *)
-    "__builtin_memcpy_aligned",
-         (TVoid [],
-           [TPtr(TVoid [], []); 
-            TPtr(TVoid [AConst], []); 
-            TInt(Cutil.size_t_ikind, []);
-            TInt(Cutil.size_t_ikind, [])],
-          false);
     (* Annotations *)
     "__builtin_annot",
         (TVoid [],
@@ -200,36 +192,6 @@ let register_annotation_val txt targ =
   Evalof(Evar(intern_string fun_name, Tfunction(targs, tres)),
          Tfunction(targs, tres))
 
-(** ** Handling of inlined memcpy functions *)
-
-let register_inlined_memcpy sz al =
-  let al =
-    if al <= 4l then al else 4l in (* max alignment supported by CompCert *)
-  let name = Printf.sprintf "__builtin_memcpy_sz%ld_al%ld" sz al in
-  let targs = Tcons(Tpointer(Tvoid, noattr),
-              Tcons(Tpointer(Tvoid, noattr), Tnil))
-  and tres = Tvoid
-  and ef = EF_memcpy(coqint_of_camlint sz, coqint_of_camlint al) in
-  register_special_external name ef targs tres;
-  Evalof(Evar(intern_string name, Tfunction(targs, tres)),
-         Tfunction(targs, tres))
-
-let make_builtin_memcpy args =
-  match args with
-  | Econs(dst, Econs(src, Econs(sz, Econs(al, Enil)))) ->
-      let sz1 =
-        match Initializers.constval sz with
-        | CompcertErrors.OK(Vint n) -> camlint_of_coqint n
-        | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be a constant)"; 0l in
-      let al1 =
-        match Initializers.constval al with
-        | CompcertErrors.OK(Vint n) -> camlint_of_coqint n
-        | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be a constant)"; 0l in
-      let fn = register_inlined_memcpy sz1 al1 in
-      Ecall(fn, Econs(dst, Econs(src, Enil)), Tvoid)
-  | _ ->
-    assert false
-
 (** ** Translation functions *)
 
 (** Constants *)
@@ -550,9 +512,6 @@ let rec convertExpr env e =
           ezero
       end          
 
- | C.ECall({edesc = C.EVar {name = "__builtin_memcpy_aligned"}}, args) ->
-      make_builtin_memcpy (convertExprList env args)
-
   | C.ECall(fn, args) ->
       match projFunType env fn.etyp with
       | None ->
@@ -588,14 +547,14 @@ and convertLvalue env e =
   | C.EUnop(C.Oderef, e1) ->
       Ederef(convertExpr env e1, ty)
   | C.EUnop(C.Odot id, e1) ->
-      Efield(convertLvalue env e1, intern_string id, ty)
+      Efield(convertExpr env e1, intern_string id, ty)
   | C.EUnop(C.Oarrow id, e1) ->
       let e1' = convertExpr env e1 in
       let ty1 =
         match typeof e1' with
         | Tpointer(t, _) -> t
         | _ -> error ("wrong type for ->" ^ id ^ " access"); Tvoid in
-      Efield(Ederef(e1', ty1), intern_string id, ty)
+      Efield(Evalof(Ederef(e1', ty1), ty1), intern_string id, ty)
   | C.EBinop(C.Oindex, e1, e2, _) ->
       coq_Eindex (convertExpr env e1) (convertExpr env e2) ty
   | _ ->
@@ -784,7 +743,9 @@ let convertInitializer env ty i =
   match Initializers.transl_init (convertTyp env ty) (convertInit env i)
   with
   | CompcertErrors.OK init -> init
-  | CompcertErrors.Error msg -> error (string_of_errmsg msg); []
+  | CompcertErrors.Error msg ->
+      error (sprintf "Initializer is not a compile-time constant (%s)"
+                     (string_of_errmsg msg)); []
 
 (** Global variable *)
 
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index e9c40a2..9690ba8 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -58,8 +58,8 @@ Fixpoint constval (a: expr) : res val :=
       end
   | Evalof l ty =>
       match access_mode ty with
-      | By_reference => constval l
-      | _ => Error(msg "dereference operation")
+      | By_reference | By_copy => constval l
+      | _ => Error(msg "dereferencing of an l-value")
       end
   | Eaddrof l ty =>
       constval l
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 4d287bc..057933e 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -445,7 +445,7 @@ Proof.
   (* val *)
   destruct v; monadInv CV; constructor.
   (* rval *)
-  inv H1; rewrite H2 in CV; try congruence. eauto. 
+  inv H1; rewrite H2 in CV; try congruence. eauto. eauto. 
   (* addrof *)
   eauto.
   (* unop *)