- Support for _Alignof(ty) operator from ISO C 2011

  and __alignof__(ty), __alignof__(expr) from GCC.
- Resurrected __builtin_memcpy_aligned, useful for files generated
  by Scade KCG 6.



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

15 files changed, 102 insertions, 14 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index d7f4aff..1abf332 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -77,6 +77,14 @@ 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 [],
@@ -195,6 +203,38 @@ 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 *)
@@ -367,6 +407,8 @@ let rec convertExpr env e =
       Eval(Vint(convertInt i), ty)
   | C.ESizeof ty1 ->
       Esizeof(convertTyp env ty1, ty)
+  | C.EAlignof ty1 ->
+      Ealignof(convertTyp env ty1, ty)
 
   | C.EUnop(C.Ominus, e1) ->
       Eunop(Oneg, convertExpr env e1, ty)
@@ -475,6 +517,9 @@ 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 ->
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index b3c3f6b..f589fab 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -787,6 +787,8 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       end
   | RV, Esizeof ty' ty =>
       topred (Rred (Eval (Vint (Int.repr (sizeof ty'))) ty) m E0)
+  | RV, Ealignof ty' ty =>
+      topred (Rred (Eval (Vint (Int.repr (alignof ty'))) ty) m E0)
   | RV, Eassign l1 r2 ty =>
       match is_loc l1, is_val r2 with
       | Some(b, ofs, ty1), Some(v2, ty2) =>
@@ -1363,6 +1365,8 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   eapply incontext_ok; eauto.
 (* sizeof *)
   apply topred_ok; auto. split. apply red_sizeof. exists w; constructor.
+(* alignof *)
+  apply topred_ok; auto. split. apply red_alignof. exists w; constructor.
 (* assign *)
   destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn. 
   destruct (is_val a2) as [[v2 ty2] | ]_eqn. 
@@ -1494,6 +1498,8 @@ Proof.
   inv H0. rewrite H; auto.
 (* sizeof *)
   inv H. auto.
+(* alignof *)
+  inv H. auto.
 (* assign *)
   rewrite dec_eq_true; auto. rewrite H. rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H1). auto.
 (* assignop *)
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index f0073a1..e4c451b 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -57,9 +57,13 @@ Inductive expr : Type :=
   | Ebinop: binary_operation -> expr -> expr -> type -> expr (**r binary operation *)
   | Ecast: expr -> type -> expr   (**r type cast ([(ty) e]) *)
   | Econdition: expr -> expr -> expr -> type -> expr (**r conditional ([e1 ? e2 : e3]) *)
-  | Esizeof: type -> type -> expr         (**r size of a type *)
   | Efield: expr -> ident -> type -> expr. (**r access to a member of a struct or union *)
 
+(** [sizeof] and [alignof] are derived forms. *)
+
+Definition Esizeof (ty' ty: type) : expr := Econst_int (Int.repr(sizeof ty')) ty.
+Definition Ealignof (ty' ty: type) : expr := Econst_int (Int.repr(alignof ty')) ty.
+
 (** Extract the type part of a type-annotated Clight expression. *)
 
 Definition typeof (e: expr) : type :=
@@ -74,7 +78,6 @@ Definition typeof (e: expr) : type :=
   | Ebinop _ _ _ ty => ty
   | Ecast _ ty => ty
   | Econdition _ _ _ ty => ty
-  | Esizeof _ ty => ty
   | Efield _ _ ty => ty
   end.
 
@@ -238,8 +241,6 @@ Inductive eval_expr: expr -> val -> Prop :=
   | eval_Eaddrof: forall a ty loc ofs,
       eval_lvalue a loc ofs ->
       eval_expr (Eaddrof a ty) (Vptr loc ofs)
-  | eval_Esizeof: forall ty' ty,
-      eval_expr (Esizeof ty' ty) (Vint (Int.repr (sizeof ty')))
   | eval_Eunop:  forall op a ty v1 v,
       eval_expr a v1 ->
       sem_unary_operation op v1 (typeof a) = Some v ->
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 49b2062..9087aa4 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -734,6 +734,9 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
   | red_sizeof: forall ty1 ty m,
       rred (Esizeof ty1 ty) m
         E0 (Eval (Vint (Int.repr (sizeof ty1))) ty) m
+  | red_alignof: forall ty1 ty m,
+      rred (Ealignof ty1 ty) m
+        E0 (Eval (Vint (Int.repr (alignof ty1))) ty) m
   | red_assign: forall b ofs ty1 v2 ty2 m v t m',
       sem_cast v2 ty2 ty1 = Some v ->
       assign_loc ge ty1 m b ofs v t m' ->
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index c17d79e..3145681 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -403,8 +403,6 @@ Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr :=
       OK(Econdition (make_boolean tb (typeof b))
                     (make_cast (typeof c) ty tc)
                     (make_cast (typeof d) ty td))
-  | Clight.Esizeof ty _ =>
-      OK(make_intconst (Int.repr (Csyntax.sizeof ty)))
   | Clight.Efield b i ty => 
       match typeof b with
       | Tstruct _ fld _ =>
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 1089b6b..0b8b9a0 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -1216,8 +1216,6 @@ Proof.
   constructor; auto.
 (* addrof *)
   simpl in TR. auto. 
-(* sizeof *)
-  constructor; auto.
 (* unop *)
   eapply transl_unop_correct; eauto.
 (* binop *)
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index 4bb550f..13cffb5 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -58,6 +58,7 @@ Fixpoint simple (a: expr) : bool :=
   | Ecast r1 _ => simple r1
   | Econdition r1 r2 r3 _ => simple r1 && simple r2 && simple r3
   | Esizeof _ _ => true
+  | Ealignof _ _ => true
   | Eassign _ _ _ => false
   | Eassignop _ _ _ _ _ => false
   | Epostincr _ _ _ => false
@@ -133,7 +134,9 @@ with eval_simple_rvalue: expr -> val -> Prop :=
       sem_cast v2 (typeof (if b then r2 else r3)) ty = Some v ->
       eval_simple_rvalue (Econdition r1 r2 r3 ty) v
   | esr_sizeof: forall ty1 ty,
-      eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1))).
+      eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1)))
+  | esr_alignof: forall ty1 ty,
+      eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ty1))).
 
 Inductive eval_simple_list: exprlist -> typelist -> list val -> Prop :=
   | esrl_nil:
@@ -686,6 +689,8 @@ Ltac FinishL := apply star_one; left; apply step_lred; eauto; simpl; try (econst
   FinishR. auto.
 (* sizeof *)
   FinishR.
+(* alignof *)
+  FinishR.
 (* loc *)
   apply star_refl.
 (* var local *)
@@ -815,6 +820,8 @@ Ltac StepR REC C' a :=
   exists v2. econstructor; eauto. 
 (* sizeof *)
   econstructor; econstructor.
+(* alignof *)
+  econstructor; econstructor.
 (* loc *)
   exists b; exists ofs; constructor.
 Qed.
@@ -1585,6 +1592,8 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty)
   | eval_sizeof: forall e m ty' ty,
       eval_expr e m RV (Esizeof ty' ty) E0 m (Esizeof ty' ty)
+  | eval_alignof: forall e m ty' ty,
+      eval_expr e m RV (Ealignof ty' ty) E0 m (Ealignof ty' ty)
   | eval_assign: forall e m l r ty t1 m1 l' t2 m2 r' b ofs v v' t3 m3,
       eval_expr e m LV l t1 m1 l' -> eval_expr e m1 RV r t2 m2 r' ->
       eval_simple_lvalue ge e m2 l' b ofs ->
@@ -2114,6 +2123,8 @@ Proof.
   reflexivity. reflexivity. traceEq.
 (* sizeof *)
   simpl; intuition. apply star_refl.
+(* alignof *)
+  simpl; intuition. apply star_refl.
 (* assign *)
   exploit (H0 (fun x => C(Eassign x r ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]].
@@ -2479,6 +2490,7 @@ Fixpoint esize (a: expr) : nat :=
   | Ecast r1 _ => S(esize r1)
   | Econdition r1 _ _ _ => S(esize r1)
   | Esizeof _ _ => 1%nat
+  | Ealignof _ _ => 1%nat
   | Eassign l1 r2 _ => S(esize l1 + esize r2)%nat
   | Eassignop _ l1 r2 _ _ => S(esize l1 + esize r2)%nat
   | Epostincr _ l1 _ => S(esize l1)
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index ffe08bf..e9e260b 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -210,6 +210,7 @@ Inductive expr : Type :=
   | Ecast (r: expr) (ty: type)                        (**r type cast [(ty)r] *)
   | Econdition (r1 r2 r3: expr) (ty: type)  (**r conditional [r1 ? r2 : r3] *)
   | Esizeof (ty': type) (ty: type)                      (**r size of a type *)
+  | Ealignof (ty': type) (ty: type)        (**r natural alignment of a type *)
   | Eassign (l: expr) (r: expr) (ty: type)          (**r assignment [l = r] *)
   | Eassignop (op: binary_operation) (l: expr) (r: expr) (tyres ty: type)
                                   (**r assignment with arithmetic [l op= r] *)
@@ -296,6 +297,7 @@ Definition typeof (a: expr) : type :=
   | Ecast _ ty => ty
   | Econdition _ _ _ ty => ty
   | Esizeof _ ty => ty
+  | Ealignof _ ty => ty
   | Eassign _ _ ty => ty
   | Eassignop _ _ _ _ ty => ty
   | Epostincr _ _ ty => ty
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index 9690ba8..b4e3984 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -80,6 +80,8 @@ Fixpoint constval (a: expr) : res val :=
       do v1 <- constval r; do_cast v1 (typeof r) ty
   | Esizeof ty1 ty =>
       OK (Vint (Int.repr (sizeof ty1)))
+  | Ealignof ty1 ty =>
+      OK (Vint (Int.repr (alignof ty1)))
   | Econdition r1 r2 r3 ty =>
       do v1 <- constval r1;
       do v2 <- constval r2;
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 057933e..627db89 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -53,6 +53,7 @@ Fixpoint simple (a: expr) : Prop :=
   | Ecast r1 _ => simple r1
   | Econdition r1 r2 r3 _ => simple r1 /\ simple r2 /\ simple r3
   | Esizeof _ _ => True
+  | Ealignof _ _ => True
   | Eassign _ _ _ => False
   | Eassignop _ _ _ _ _ => False
   | Epostincr _ _ _ => False
@@ -120,6 +121,8 @@ with eval_simple_rvalue: expr -> val -> Prop :=
       eval_simple_rvalue (Ecast r1 ty) v
   | esr_sizeof: forall ty1 ty,
       eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1)))
+  | esr_alignof: forall ty1 ty,
+      eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ty1)))
   | esr_condition: forall r1 r2 r3 ty v v1 b v',
       eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some b -> 
       eval_simple_rvalue (if b then r2 else r3) v' ->
@@ -184,6 +187,7 @@ Proof.
   inv EV. econstructor; eauto. constructor.
   inv EV. eapply esr_condition; eauto. constructor. 
   inv EV. constructor.
+  inv EV. constructor.
   econstructor; eauto. constructor.
   inv EV. econstructor. constructor. auto. 
 Qed.
@@ -458,6 +462,8 @@ Proof.
   eapply sem_cast_match; eauto. 
   (* sizeof *)
   constructor.
+  (* alignof *)
+  constructor.
   (* conditional *)
   rewrite (bool_val_match x v1 (typeof r1)) in EQ3; auto.
   rewrite H0 in EQ3. destruct b; eapply sem_cast_match; eauto.
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index 77f22f7..1bd21da 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -54,7 +54,6 @@ let rec precedence = function
   | Efield _ -> (16, LtoR)
   | Econst_int _ -> (16, NA)
   | Econst_float _ -> (16, NA)
-  | Esizeof _ -> (15, RtoL)
   | Eunop _ -> (15, RtoL)
   | Eaddrof _ -> (15, RtoL)
   | Ecast _ -> (14, RtoL)
@@ -92,8 +91,6 @@ let rec expr p (prec, e) =
       fprintf p "%ld" (camlint_of_coqint n)
   | Econst_float(f, _) ->
       fprintf p "%F" f
-  | Esizeof(ty, _) ->
-      fprintf p "sizeof(%s)" (name_type ty)
   | Eunop(op, a1, _) ->
       fprintf p "%s%a" (name_unop op) expr (prec', a1)
   | Eaddrof(a1, _) ->
@@ -268,7 +265,6 @@ let rec collect_expr = function
   | Ecast(r, _) -> collect_expr r
   | Econdition(r1, r2, r3, _) -> 
       collect_expr r1; collect_expr r2; collect_expr r3
-  | Esizeof _ -> ()
 
 let rec collect_exprlist = function
   | [] -> ()
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 804b018..0616049 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -145,6 +145,7 @@ let rec precedence = function
   | Eval _ -> (16, NA)
   | Evalof(l, _) -> precedence l
   | Esizeof _ -> (15, RtoL)
+  | Ealignof _ -> (15, RtoL)
   | Ecall _ -> (16, LtoR)
   | Epostincr _ -> (16, LtoR)
   | Eunop _ -> (15, RtoL)
@@ -196,6 +197,8 @@ let rec expr p (prec, e) =
       fprintf p "<undef>"
   | Esizeof(ty, _) ->
       fprintf p "sizeof(%s)" (name_type ty)
+  | Ealignof(ty, _) ->
+      fprintf p "__alignof__(%s)" (name_type ty)
   | Eunop(op, a1, _) ->
       fprintf p "%s%a" (name_unop op) expr (prec', a1)
   | Eaddrof(a1, _) ->
@@ -444,7 +447,8 @@ let rec collect_expr = function
   | Ecast(r, _) -> collect_expr r
   | Econdition(r1, r2, r3, _) -> 
       collect_expr r1; collect_expr r2; collect_expr r3
-  | Esizeof _ -> ()
+  | Esizeof(ty, _) -> collect_type ty
+  | Ealignof(ty, _) -> collect_type ty
   | Eassign(l, r, _) -> collect_expr l; collect_expr r
   | Eassignop(_, l, r, _, _) -> collect_expr l; collect_expr r
   | Epostincr(_, l, _) -> collect_expr l
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 7b37692..3144b65 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -214,6 +214,8 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr
       error (msg "SimplExpr.transl_expr: val")
   | C.Esizeof ty' ty =>
       ret (finish dst nil (Esizeof ty' ty))
+  | C.Ealignof ty' ty =>
+      ret (finish dst nil (Ealignof ty' ty))
   | C.Evalof l ty =>
       do (sl1, a1) <- transl_expr For_val l;
       do (sl2, a2) <- transl_valof (C.typeof l) a1;
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index a88e4c3..868f7ab 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -243,6 +243,11 @@ Opaque makeif.
   split; auto. split; auto. constructor.
   auto.
   exists (Esizeof ty1 ty). split. auto. split. auto. constructor.
+(* alignof *)
+  destruct dst.
+  split; auto. split; auto. constructor.
+  auto.
+  exists (Ealignof ty1 ty). split. auto. split. auto. constructor.
 (* var local *)
   split; auto. split; auto. apply eval_Evar_local; auto. 
 (* var global *)
@@ -1280,6 +1285,7 @@ Fixpoint esize (a: C.expr) : nat :=
   | C.Ecast r1 _ => S(esize r1)
   | C.Econdition r1 _ _ _ => S(esize r1)
   | C.Esizeof _ _ => 1%nat
+  | C.Ealignof _ _ => 1%nat
   | C.Eassign l1 r2 _ => S(esize l1 + esize r2)%nat
   | C.Eassignop _ l1 r2 _ _ => S(esize l1 + esize r2)%nat
   | C.Epostincr _ l1 _ => S(esize l1)
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 647e048..bd7f336 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -89,6 +89,10 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -
       tr_expr le dst (C.Esizeof ty' ty)
                    (final dst (Esizeof ty' ty))
                    (Esizeof ty' ty) tmp
+  | tr_alignof: forall le dst ty' ty tmp,
+      tr_expr le dst (C.Ealignof ty' ty)
+                   (final dst (Ealignof ty' ty))
+                   (Ealignof ty' ty) tmp
   | tr_valof: forall le dst e1 ty tmp sl1 a1 tmp1 sl2 a2 tmp2,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_rvalof (C.typeof e1) a1 sl2 a2 tmp2 ->
@@ -719,6 +723,9 @@ Opaque makeif.
 (* sizeof *)
   monadInv H. UseFinish.
   exists (@nil ident); split; auto with gensym. constructor.
+(* alignof *)
+  monadInv H. UseFinish.
+  exists (@nil ident); split; auto with gensym. constructor.
 (* assign *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [C D]].