From 2570ddd61b1c98b62c8d97fce862654535696844 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 26 Feb 2012 10:41:07 +0000 Subject: - 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 --- cfrontend/C2C.ml | 45 +++++++++++++++++++++++++++++++++++++++++++ cfrontend/Cexec.v | 6 ++++++ cfrontend/Clight.v | 9 +++++---- cfrontend/Csem.v | 3 +++ cfrontend/Cshmgen.v | 2 -- cfrontend/Cshmgenproof.v | 2 -- cfrontend/Cstrategy.v | 14 +++++++++++++- cfrontend/Csyntax.v | 2 ++ cfrontend/Initializers.v | 2 ++ cfrontend/Initializersproof.v | 6 ++++++ cfrontend/PrintClight.ml | 4 ---- cfrontend/PrintCsyntax.ml | 6 +++++- cfrontend/SimplExpr.v | 2 ++ cfrontend/SimplExprproof.v | 6 ++++++ cfrontend/SimplExprspec.v | 7 +++++++ 15 files changed, 102 insertions(+), 14 deletions(-) (limited to 'cfrontend') 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 "" | 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]]. -- cgit v1.2.3