summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-02-26 10:41:07 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-02-26 10:41:07 +0000
commit2570ddd61b1c98b62c8d97fce862654535696844 (patch)
treee9a652b115045a3b2c4ade69ec3cc3fdad429b54
parent65cc3738e7436e46f70c0508638a71fbb49c50a8 (diff)
- 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
-rw-r--r--.depend4
-rw-r--r--Changelog4
-rw-r--r--cfrontend/C2C.ml45
-rw-r--r--cfrontend/Cexec.v6
-rw-r--r--cfrontend/Clight.v9
-rw-r--r--cfrontend/Csem.v3
-rw-r--r--cfrontend/Cshmgen.v2
-rw-r--r--cfrontend/Cshmgenproof.v2
-rw-r--r--cfrontend/Cstrategy.v14
-rw-r--r--cfrontend/Csyntax.v2
-rw-r--r--cfrontend/Initializers.v2
-rw-r--r--cfrontend/Initializersproof.v6
-rw-r--r--cfrontend/PrintClight.ml4
-rw-r--r--cfrontend/PrintCsyntax.ml6
-rw-r--r--cfrontend/SimplExpr.v2
-rw-r--r--cfrontend/SimplExprproof.v6
-rw-r--r--cfrontend/SimplExprspec.v7
-rw-r--r--cparser/Bitfields.ml1
-rw-r--r--cparser/C.mli1
-rw-r--r--cparser/Ceval.ml5
-rw-r--r--cparser/Cleanup.ml1
-rw-r--r--cparser/Cprint.ml2
-rw-r--r--cparser/Elab.ml31
-rw-r--r--cparser/Lexer.mll1
-rw-r--r--cparser/PackedStructs.ml1
-rw-r--r--cparser/Rename.ml1
-rw-r--r--cparser/StructReturn.ml2
27 files changed, 134 insertions, 36 deletions
diff --git a/.depend b/.depend
index bebd789..3d6e10c 100644
--- a/.depend
+++ b/.depend
@@ -95,8 +95,8 @@ cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axiom
cfrontend/Cexec.vo cfrontend/Cexec.glob: cfrontend/Cexec.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo
cfrontend/Initializers.vo cfrontend/Initializers.glob: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo
-cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Clight.vo
-cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo
+cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo
+cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo
cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob: cfrontend/SimplExprproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo
cfrontend/Clight.vo cfrontend/Clight.glob: cfrontend/Clight.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
cfrontend/Cshmgen.vo cfrontend/Cshmgen.glob: cfrontend/Cshmgen.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo
diff --git a/Changelog b/Changelog
index 761fd7a..3855365 100644
--- a/Changelog
+++ b/Changelog
@@ -1,4 +1,4 @@
-Release 1.10, 2012-02-15
+Release 1.10, 2012-02-28
========================
Improvements in confidence:
@@ -13,6 +13,8 @@ Improvements in confidence:
Language features:
- Support for _Bool type from ISO C99.
+- Support for _Alignof(ty) operator from ISO C 2011
+ and __alignof__(ty), __alignof__(expr) from GCC.
Performance improvements:
- Improvements in instruction selection, especially for integer casts
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]].
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index c1b83cb..257f6c8 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -235,6 +235,7 @@ let transf_expr env ctx e =
match e.edesc with
| EConst _ -> e
| ESizeof _ -> e
+ | EAlignof _ -> e
| EVar _ -> e
| EUnop(Odot s, e1) ->
diff --git a/cparser/C.mli b/cparser/C.mli
index 35e872d..52f02c4 100644
--- a/cparser/C.mli
+++ b/cparser/C.mli
@@ -151,6 +151,7 @@ type exp = { edesc: exp_desc; etyp: typ }
and exp_desc =
| EConst of constant
| ESizeof of typ
+ | EAlignof of typ
| EVar of ident
| EUnop of unary_operator * exp
| EBinop of binary_operator * exp * exp * typ
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index fbeb522..4fc01e5 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -246,6 +246,11 @@ let rec expr env e =
| None -> raise Notconst
| Some n -> I(Int64.of_int n)
end
+ | EAlignof ty ->
+ begin match alignof env ty with
+ | None -> raise Notconst
+ | Some n -> I(Int64.of_int n)
+ end
| EVar _ ->
raise Notconst
| EUnop(op, e1) ->
diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
index 17b2f98..54dfd67 100644
--- a/cparser/Cleanup.ml
+++ b/cparser/Cleanup.ml
@@ -58,6 +58,7 @@ let rec add_exp e =
| EConst (CEnum(id, v)) -> addref id
| EConst _ -> ()
| ESizeof ty -> add_typ ty
+ | EAlignof ty -> add_typ ty
| EVar id -> addref id
| EUnop(op, e1) -> add_exp e1
| EBinop(op, e1, e2, ty) -> add_exp e1; add_exp e2
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 5887e87..2924c3d 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -181,6 +181,7 @@ type associativity = LtoR | RtoL | NA
let precedence = function (* H&S section 7.2 *)
| EConst _ -> (16, NA)
| ESizeof _ -> (15, RtoL)
+ | EAlignof _ -> (15, RtoL)
| EVar _ -> (16, NA)
| EBinop(Oindex, _, _, _) -> (16, LtoR)
| ECall _ -> (16, LtoR)
@@ -215,6 +216,7 @@ let rec exp pp (prec, a) =
| EConst cst -> const pp cst
| EVar id -> ident pp id
| ESizeof ty -> fprintf pp "sizeof(%a)" typ ty
+ | EAlignof ty -> fprintf pp "__alignof(%a)" typ ty
| EUnop(Ominus, a1) ->
fprintf pp "-%a" exp (prec', a1)
| EUnop(Oplus, a1) ->
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 2da1936..f9b70c4 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -867,6 +867,18 @@ let elab_expr loc env a =
err "incomplete type %a" Cprint.typ ty;
{ edesc = ESizeof ty; etyp = TInt(size_t_ikind, []) }
+ | EXPR_ALIGNOF a1 ->
+ let b1 = elab a1 in
+ if sizeof env b1.etyp = None then
+ err "incomplete type %a" Cprint.typ b1.etyp;
+ { edesc = EAlignof b1.etyp; etyp = TInt(size_t_ikind, []) }
+
+ | TYPE_ALIGNOF (spec, dcl) ->
+ let ty = elab_type loc env spec dcl in
+ if sizeof env ty = None then
+ err "incomplete type %a" Cprint.typ ty;
+ { edesc = EAlignof ty; etyp = TInt(size_t_ikind, []) }
+
| UNARY(PLUS, a1) ->
let b1 = elab a1 in
if not (is_arith_type env b1.etyp) then
@@ -1110,25 +1122,6 @@ let elab_expr loc env a =
error "GCC's &&label construct is not supported"
| GNU_BODY _ ->
error "GCC's statements within expressions are not supported"
- | EXPR_ALIGNOF _ | TYPE_ALIGNOF _ ->
- error "GCC's __alignof__ construct is not supported"
-
-(*
- | EXPR_ALIGNOF a1 ->
- warning "nonstandard `alignof' expression, turned into a constant";
- let b1 = elab a1 in
- begin match alignof env b1.etyp with
- | None -> error "incomplete type %a" Cprint.typ b1.etyp
- | Some al -> intconst (Int64.of_int al) size_t_ikind
- end
- | TYPE_ALIGNOF (spec, dcl) ->
- warning "nonstandard `alignof' expression, turned into a constant";
- let ty = elab_type loc env spec dcl in
- begin match alignof env ty with
- | None -> error "incomplete type %a" Cprint.typ ty
- | Some al -> intconst (Int64.of_int al) size_t_ikind
- end
-*)
(* Elaboration of pre- or post- increment/decrement *)
and elab_pre_post_incr_decr op msg a1 =
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index d4947ad..ab90bc2 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -145,6 +145,7 @@ let init_lexicon _ =
("__typeof__", fun loc -> TYPEOF loc);
("__typeof", fun loc -> TYPEOF loc);
("typeof", fun loc -> TYPEOF loc);
+ ("_Alignof", fun loc -> ALIGNOF loc);
("__alignof", fun loc -> ALIGNOF loc);
("__alignof__", fun loc -> ALIGNOF loc);
("__volatile__", fun loc -> VOLATILE loc);
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index 30466cb..ebdd86b 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -251,6 +251,7 @@ let transf_expr loc env ctx e =
match e.edesc with
| EConst _ -> e
| ESizeof _ -> e
+ | EAlignof _ -> e
| EVar _ -> e
| EUnop(Odot _, _) | EUnop(Oarrow _, _) | EBinop(Oindex, _, _, _) ->
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index d58c8ad..0ce401f 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -102,6 +102,7 @@ let rec exp env e =
and exp_desc env = function
| EConst cst -> EConst(constant env cst)
| ESizeof ty -> ESizeof(typ env ty)
+ | EAlignof ty -> EAlignof(typ env ty)
| EVar id -> EVar(ident env id)
| EUnop(op, a) -> EUnop(op, exp env a)
| EBinop(op, a, b, ty) -> EBinop(op, exp env a, exp env b, typ env ty)
diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml
index 57246ce..dd985b1 100644
--- a/cparser/StructReturn.ml
+++ b/cparser/StructReturn.ml
@@ -57,6 +57,8 @@ let rec transf_expr env ctx e =
{edesc = EConst c; etyp = newty}
| ESizeof ty ->
{edesc = ESizeof (transf_type env ty); etyp = newty}
+ | EAlignof ty ->
+ {edesc = EAlignof (transf_type env ty); etyp = newty}
| EVar x ->
{edesc = EVar x; etyp = newty}
| EUnop(op, e1) ->