From 884756b623fd6031a04102a545d92e4ec905f1cc Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 6 May 2013 15:25:26 +0000 Subject: Revised semantics and compilation of 2-argument C operators to better match "the usual binary conversions" and be more robust towards future extensions e.g. with 32-bit float values. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2239 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cop.v | 160 ++++++++++++++++++++--------------------------- cfrontend/Cshmgen.v | 150 ++++++++++++++++++++------------------------ cfrontend/Cshmgenproof.v | 36 +++++------ 3 files changed, 152 insertions(+), 194 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index d0853508..e7ffc891 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -449,105 +449,72 @@ Definition sem_notint (v: val) (ty: type): option val := (** ** Binary operators *) -(** For binary operations, the "usual binary conversions", adapted to a 32-bit - platform, state that: -- If both arguments are of integer type, an integer operation is performed. - For operations that behave differently at unsigned and signed types - (e.g. division, modulus, comparisons), the unsigned operation is selected - if at least one of the arguments is of type "unsigned int32", otherwise - the signed operation is performed. -- Likewise if both arguments are of long integer type. -- If both arguments are of float type, a float operation is performed. - We choose to perform all float arithmetic in double precision, - even if both arguments are single-precision floats. -- If one argument has integer/long type and the other has float type, - we convert the integer argument to float, then perform the float operation. -- If one argument has long integer type and the other integer type, - we convert the integer argument to long, then perform the long operation +(** For binary operations, the "usual binary conversions" consist in +- determining the type at which the operation is to be performed + (a form of least upper bound of the types of the two arguments); +- casting the two arguments to this common type; +- performing the operation at that type. *) Inductive binarith_cases: Type := - | bin_case_ii(s: signedness) (**r int, int *) - | bin_case_ff (**r float, float *) - | bin_case_if(s: signedness) (**r int, float *) - | bin_case_fi(s: signedness) (**r float, int *) - | bin_case_ll(s: signedness) (**r long, long *) - | bin_case_il(s1 s2: signedness) (**r int, long *) - | bin_case_li(s1 s2: signedness) (**r long, int *) - | bin_case_lf(s: signedness) (**r long, float *) - | bin_case_fl(s: signedness) (**r float, long *) - | bin_default. + | bin_case_i (s: signedness) (**r at int type *) + | bin_case_l (s: signedness) (**r at long int type *) + | bin_case_f (**r at float type *) + | bin_default. (**r error *) Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => bin_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => bin_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => bin_case_ii Signed - | Tfloat _ _, Tfloat _ _ => bin_case_ff - | Tint _ sg _, Tfloat _ _ => bin_case_if sg - | Tfloat _ _, Tint _ sg _ => bin_case_fi sg - | Tlong Signed _, Tlong Signed _ => bin_case_ll Signed - | Tlong _ _, Tlong _ _ => bin_case_ll Unsigned - | Tint _ s1 _, Tlong s2 _ => bin_case_il s1 s2 - | Tlong s1 _, Tint _ s2 _ => bin_case_li s1 s2 - | Tlong sg _, Tfloat _ _ => bin_case_lf sg - | Tfloat _ _, Tlong sg _ => bin_case_fl sg + match ty1, ty2 with + | Tint I32 Unsigned _, Tint _ _ _ => bin_case_i Unsigned + | Tint _ _ _, Tint I32 Unsigned _ => bin_case_i Unsigned + | Tint _ _ _, Tint _ _ _ => bin_case_i Signed + | Tlong Signed _, Tlong Signed _ => bin_case_l Signed + | Tlong _ _, Tlong _ _ => bin_case_l Unsigned + | Tlong sg _, Tint _ _ _ => bin_case_l sg + | Tint _ _ _, Tlong sg _ => bin_case_l sg + | Tfloat _ _, (Tint _ _ _ | Tlong _ _ | Tfloat _ _) => bin_case_f + | (Tint _ _ _ | Tlong _ _), Tfloat _ _ => bin_case_f | _, _ => bin_default end. +Definition binarith_type (c: binarith_cases) : type := + match c with + | bin_case_i sg => Tint I32 sg noattr + | bin_case_l sg => Tlong sg noattr + | bin_case_f => Tfloat F64 noattr + | bin_default => Tvoid + end. + Definition sem_binarith (sem_int: signedness -> int -> int -> option val) (sem_long: signedness -> int64 -> int64 -> option val) (sem_float: float -> float -> option val) (v1: val) (t1: type) (v2: val) (t2: type) : option val := + let c := classify_binarith t1 t2 in + let t := binarith_type c in + match sem_cast v1 t1 t with + | None => None + | Some v1' => + match sem_cast v2 t2 t with + | None => None + | Some v2' => match classify_binarith t1 t2 with - | bin_case_ii sg => - match v1, v2 with + | bin_case_i sg => + match v1', v2' with | Vint n1, Vint n2 => sem_int sg n1 n2 | _, _ => None end - | bin_case_ff => - match v1, v2 with + | bin_case_f => + match v1', v2' with | Vfloat n1, Vfloat n2 => sem_float n1 n2 | _, _ => None end - | bin_case_if sg => - match v1, v2 with - | Vint n1, Vfloat n2 => sem_float (cast_int_float sg n1) n2 - | _, _ => None - end - | bin_case_fi sg => - match v1, v2 with - | Vfloat n1, Vint n2 => sem_float n1 (cast_int_float sg n2) - | _, _ => None - end - | bin_case_ll sg => - match v1, v2 with + | bin_case_l sg => + match v1', v2' with | Vlong n1, Vlong n2 => sem_long sg n1 n2 | _, _ => None end - | bin_case_il sg1 sg2 => - match v1, v2 with - | Vint n1, Vlong n2 => sem_long sg2 (cast_int_long sg1 n1) n2 - | _, _ => None - end - | bin_case_li sg1 sg2 => - match v1, v2 with - | Vlong n1, Vint n2 => sem_long sg1 n1 (cast_int_long sg2 n2) - | _, _ => None - end - | bin_case_lf sg => - match v1, v2 with - | Vlong n1, Vfloat n2 => sem_float (cast_long_float sg n1) n2 - | _, _ => None - end - | bin_case_fl sg => - match v1, v2 with - | Vfloat n1, Vlong n2 => sem_float n1 (cast_long_float sg n2) - | _, _ => None - end | bin_default => None - end. + end end end. (** *** Addition *) @@ -957,6 +924,22 @@ Ltac TrivialInject := | _ => idtac end. +Lemma sem_cast_inject: + forall v1 ty1 ty v tv1, + sem_cast v1 ty1 ty = Some v -> + val_inject f v1 tv1 -> + exists tv, sem_cast tv1 ty1 ty = Some tv /\ val_inject f v tv. +Proof. + unfold sem_cast; intros; destruct (classify_cast ty1 ty); + inv H0; inv H; TrivialInject. +- econstructor; eauto. +- destruct (cast_float_int si2 f0); inv H1; TrivialInject. +- destruct (cast_float_long si2 f0); inv H1; TrivialInject. +- destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto. +- destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto. +- econstructor; eauto. +Qed. + Lemma sem_unary_operation_inject: forall op v1 ty v tv1, sem_unary_operation op v1 ty = Some v -> @@ -992,8 +975,15 @@ Proof. { intros. subst ov; simpl in H6. destruct v0; contradiction || constructor. } - exists v. - unfold sem_binarith in *; destruct (classify_binarith t1 t2); inv H0; inv H1; discriminate || eauto. + unfold sem_binarith in *. + set (c := classify_binarith t1 t2) in *. + set (t := binarith_type c) in *. + destruct (sem_cast v1 t1 t) as [w1|] eqn:C1; try discriminate. + destruct (sem_cast v2 t2 t) as [w2|] eqn:C2; try discriminate. + exploit (sem_cast_inject v1); eauto. intros (w1' & C1' & INJ1). + exploit (sem_cast_inject v2); eauto. intros (w2' & C2' & INJ2). + rewrite C1'; rewrite C2'. + destruct c; inv INJ1; inv INJ2; discriminate || eauto. Qed. Remark sem_shift_inject: @@ -1119,22 +1109,6 @@ Proof. - eapply sem_cmp_inj; eauto. Qed. -Lemma sem_cast_inject: - forall v1 ty1 ty v tv1, - sem_cast v1 ty1 ty = Some v -> - val_inject f v1 tv1 -> - exists tv, sem_cast tv1 ty1 ty = Some tv /\ val_inject f v tv. -Proof. - unfold sem_cast; intros; destruct (classify_cast ty1 ty); - inv H0; inv H; TrivialInject. -- econstructor; eauto. -- destruct (cast_float_int si2 f0); inv H1; TrivialInject. -- destruct (cast_float_long si2 f0); inv H1; TrivialInject. -- destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto. -- destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto. -- econstructor; eauto. -Qed. - Lemma bool_val_inject: forall v ty b tv, bool_val v ty = Some b -> diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index c45e0946..ad89a2d3 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -84,9 +84,6 @@ Definition make_longoffloat (e: expr) (sg: signedness) := | Unsigned => Eunop Olonguoffloat e end. -(** [make_boolean e ty] returns a Csharpminor expression that evaluates - to the boolean value of [e]. *) - Definition make_cmp_ne_zero (e: expr) := match e with | Ebinop (Ocmp c) e1 e2 => e @@ -97,6 +94,49 @@ Definition make_cmp_ne_zero (e: expr) := | _ => Ebinop (Ocmp Cne) e (make_intconst Int.zero) end. +(** [make_cast from to e] applies to [e] the numeric conversions needed + to transform a result of type [from] to a result of type [to]. *) + +Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) := + match sz, si with + | I8, Signed => Eunop Ocast8signed e + | I8, Unsigned => Eunop Ocast8unsigned e + | I16, Signed => Eunop Ocast16signed e + | I16, Unsigned => Eunop Ocast16unsigned e + | I32, _ => e + | IBool, _ => make_cmp_ne_zero e + end. + +Definition make_cast_float (e: expr) (sz: floatsize) := + match sz with + | F32 => Eunop Osingleoffloat e + | F64 => e + end. + +Definition make_cast (from to: type) (e: expr) := + match classify_cast from to with + | cast_case_neutral => OK e + | cast_case_i2i sz2 si2 => OK (make_cast_int e sz2 si2) + | cast_case_f2f sz2 => OK (make_cast_float e sz2) + | cast_case_i2f si1 sz2 => OK (make_cast_float (make_floatofint e si1) sz2) + | cast_case_f2i sz2 si2 => OK (make_cast_int (make_intoffloat e si2) sz2 si2) + | cast_case_l2l => OK e + | cast_case_i2l si1 => OK (make_longofint e si1) + | cast_case_l2i sz2 si2 => OK (make_cast_int (Eunop Ointoflong e) sz2 si2) + | cast_case_l2f si1 sz2 => OK (make_cast_float (make_floatoflong e si1) sz2) + | cast_case_f2l si2 => OK (make_longoffloat e si2) + | cast_case_f2bool => OK (Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)) + | cast_case_l2bool => OK (Ebinop (Ocmpl Cne) e (make_longconst Int64.zero)) + | cast_case_p2bool => OK (Ebinop (Ocmpu Cne) e (make_intconst Int.zero)) + | cast_case_struct id1 fld1 id2 fld2 => OK e + | cast_case_union id1 fld1 id2 fld2 => OK e + | cast_case_void => OK e + | cast_case_default => Error (msg "Cshmgen.make_cast") + end. + +(** [make_boolean e ty] returns a Csharpminor expression that evaluates + to the boolean value of [e]. *) + Definition make_boolean (e: expr) (ty: type) := match classify_bool ty with | bool_case_i => make_cmp_ne_zero e @@ -106,6 +146,8 @@ Definition make_boolean (e: expr) (ty: type) := | bool_default => e (**r should not happen *) end. +(** Unary operators *) + Definition make_notbool (e: expr) (ty: type) := match classify_bool ty with | bool_case_i => OK (Ebinop (Ocmp Ceq) e (make_intconst Int.zero)) @@ -130,22 +172,20 @@ Definition make_notint (e: expr) (ty: type) := | _ => Error (msg "Cshmgen.make_notint") end. +(** Binary operators *) + Definition make_binarith (iop iopu fop lop lopu: binary_operation) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - match classify_binarith ty1 ty2 with - | bin_case_ii Signed => OK (Ebinop iop e1 e2) - | bin_case_ii Unsigned => OK (Ebinop iopu e1 e2) - | bin_case_ff => OK (Ebinop fop e1 e2) - | bin_case_if sg => OK (Ebinop fop (make_floatofint e1 sg) e2) - | bin_case_fi sg => OK (Ebinop fop e1 (make_floatofint e2 sg)) - | bin_case_ll Signed => OK (Ebinop lop e1 e2) - | bin_case_ll Unsigned => OK (Ebinop lopu e1 e2) - | bin_case_il sg1 Signed => OK (Ebinop lop (make_longofint e1 sg1) e2) - | bin_case_il sg1 Unsigned => OK (Ebinop lopu (make_longofint e1 sg1) e2) - | bin_case_li Signed sg2 => OK (Ebinop lop e1 (make_longofint e2 sg2)) - | bin_case_li Unsigned sg2 => OK (Ebinop lopu e1 (make_longofint e2 sg2)) - | bin_case_lf sg => OK (Ebinop fop (make_floatoflong e1 sg) e2) - | bin_case_fl sg => OK (Ebinop fop e1 (make_floatoflong e2 sg)) + let c := classify_binarith ty1 ty2 in + let ty := binarith_type c in + do e1' <- make_cast ty1 ty e1; + do e2' <- make_cast ty2 ty e2; + match c with + | bin_case_i Signed => OK (Ebinop iop e1' e2') + | bin_case_i Unsigned => OK (Ebinop iopu e1' e2') + | bin_case_f => OK (Ebinop fop e1' e2') + | bin_case_l Signed => OK (Ebinop lop e1' e2') + | bin_case_l Unsigned => OK (Ebinop lopu e1' e2') | bin_default => Error (msg "Cshmgen.make_binarith") end. @@ -190,16 +230,16 @@ Definition make_div (e1: expr) (ty1: type) (e2: expr) (ty2: type) := Definition make_binarith_int (iop iopu lop lopu: binary_operation) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - match classify_binarith ty1 ty2 with - | bin_case_ii Signed => OK (Ebinop iop e1 e2) - | bin_case_ii Unsigned => OK (Ebinop iopu e1 e2) - | bin_case_ll Signed => OK (Ebinop lop e1 e2) - | bin_case_ll Unsigned => OK (Ebinop lopu e1 e2) - | bin_case_il sg1 Signed => OK (Ebinop lop (make_longofint e1 sg1) e2) - | bin_case_il sg1 Unsigned => OK (Ebinop lopu (make_longofint e1 sg1) e2) - | bin_case_li Signed sg2 => OK (Ebinop lop e1 (make_longofint e2 sg2)) - | bin_case_li Unsigned sg2 => OK (Ebinop lopu e1 (make_longofint e2 sg2)) - | _ => Error (msg "Cshmgen.make_binarith_int") + let c := classify_binarith ty1 ty2 in + let ty := binarith_type c in + do e1' <- make_cast ty1 ty e1; + do e2' <- make_cast ty2 ty e2; + match c with + | bin_case_i Signed => OK (Ebinop iop e1' e2') + | bin_case_i Unsigned => OK (Ebinop iopu e1' e2') + | bin_case_l Signed => OK (Ebinop lop e1' e2') + | bin_case_l Unsigned => OK (Ebinop lopu e1' e2') + | bin_case_f | bin_default => Error (msg "Cshmgen.make_binarith_int") end. Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) := @@ -214,22 +254,6 @@ Definition make_or (e1: expr) (ty1: type) (e2: expr) (ty2: type) := Definition make_xor (e1: expr) (ty1: type) (e2: expr) (ty2: type) := make_binarith_int Oxor Oxor Oxorl Oxorl e1 ty1 e2 ty2. -(* -Definition make_shift (iop iopu lop lopu: binary_operation) - (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - match classify_shift ty1 ty2 with - | shift_case_ii Signed => OK (Ebinop iop e1 e2) - | shift_case_ii Unsigned => OK (Ebinop iopu e1 e2) - | shift_case_li Signed => OK (Ebinop lop e1 e2) - | shift_case_li Unsigned => OK (Ebinop lopu e1 e2) - | shift_case_il Signed => OK (Ebinop iop e1 (Eunop Ointoflong e2)) - | shift_case_il Unsigned => OK (Ebinop iopu e1 (Eunop Ointoflong e2)) - | shift_case_ll Signed => OK (Ebinop lop e1 (Eunop Ointoflong e2)) - | shift_case_ll Unsigned => OK (Ebinop lopu e1 (Eunop Ointoflong e2)) - | shift_default => Error (msg "Cshmgen.make_shift") - end. -*) - Definition make_shl (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_shift ty1 ty2 with | shift_case_ii _ => OK (Ebinop Oshl e1 e2) @@ -261,46 +285,6 @@ Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type make_binarith (Ocmp c) (Ocmpu c) (Ocmpf c) (Ocmpl c) (Ocmplu c) e1 ty1 e2 ty2 end. -(** [make_cast from to e] applies to [e] the numeric conversions needed - to transform a result of type [from] to a result of type [to]. *) - -Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) := - match sz, si with - | I8, Signed => Eunop Ocast8signed e - | I8, Unsigned => Eunop Ocast8unsigned e - | I16, Signed => Eunop Ocast16signed e - | I16, Unsigned => Eunop Ocast16unsigned e - | I32, _ => e - | IBool, _ => make_cmp_ne_zero e - end. - -Definition make_cast_float (e: expr) (sz: floatsize) := - match sz with - | F32 => Eunop Osingleoffloat e - | F64 => e - end. - -Definition make_cast (from to: type) (e: expr) := - match classify_cast from to with - | cast_case_neutral => OK e - | cast_case_i2i sz2 si2 => OK (make_cast_int e sz2 si2) - | cast_case_f2f sz2 => OK (make_cast_float e sz2) - | cast_case_i2f si1 sz2 => OK (make_cast_float (make_floatofint e si1) sz2) - | cast_case_f2i sz2 si2 => OK (make_cast_int (make_intoffloat e si2) sz2 si2) - | cast_case_l2l => OK e - | cast_case_i2l si1 => OK (make_longofint e si1) - | cast_case_l2i sz2 si2 => OK (make_cast_int (Eunop Ointoflong e) sz2 si2) - | cast_case_l2f si1 sz2 => OK (make_cast_float (make_floatoflong e si1) sz2) - | cast_case_f2l si2 => OK (make_longoffloat e si2) - | cast_case_f2bool => OK (Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)) - | cast_case_l2bool => OK (Ebinop (Ocmpl Cne) e (make_longconst Int64.zero)) - | cast_case_p2bool => OK (Ebinop (Ocmpu Cne) e (make_intconst Int.zero)) - | cast_case_struct id1 fld1 id2 fld2 => OK e - | cast_case_union id1 fld1 id2 fld2 => OK e - | cast_case_void => OK e - | cast_case_default => Error (msg "Cshmgen.make_cast") - end. - (** [make_load addr ty_res] loads a value of type [ty_res] from the memory location denoted by the Csharpminor expression [addr]. If [ty_res] is an array or function type, returns [addr] instead, diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index de3b8df0..953e6901 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -377,21 +377,19 @@ Lemma make_binarith_correct: (sem_binarith sem_int sem_long sem_float). Proof. red; unfold make_binarith, sem_binarith; - intros until m; intros SEM MAKE EV1 EV2; - destruct (classify_binarith tya tyb); inv MAKE; - destruct va; try discriminate; destruct vb; try discriminate. + intros until m; intros SEM MAKE EV1 EV2. + set (cls := classify_binarith tya tyb) in *. + set (ty := binarith_type cls) in *. + monadInv MAKE. + destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate. + destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate. + exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'. + exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'. + destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate. - destruct s; inv H0; econstructor; eauto with cshm. rewrite iop_ok; auto. rewrite iopu_ok; auto. -- erewrite <- fop_ok in SEM; eauto with cshm. -- erewrite <- fop_ok in SEM; eauto with cshm. -- erewrite <- fop_ok in SEM; eauto with cshm. - destruct s; inv H0; econstructor; eauto with cshm. rewrite lop_ok; auto. rewrite lopu_ok; auto. -- destruct s2; inv H0; econstructor; eauto with cshm. - rewrite lop_ok; auto. rewrite lopu_ok; auto. -- destruct s1; inv H0; econstructor; eauto with cshm. - rewrite lop_ok; auto. rewrite lopu_ok; auto. -- erewrite <- fop_ok in SEM; eauto with cshm. - erewrite <- fop_ok in SEM; eauto with cshm. Qed. @@ -401,17 +399,19 @@ Lemma make_binarith_int_correct: (sem_binarith sem_int sem_long (fun x y => None)). Proof. red; unfold make_binarith_int, sem_binarith; - intros until m; intros SEM MAKE EV1 EV2; - destruct (classify_binarith tya tyb); inv MAKE; - destruct va; try discriminate; destruct vb; try discriminate. + intros until m; intros SEM MAKE EV1 EV2. + set (cls := classify_binarith tya tyb) in *. + set (ty := binarith_type cls) in *. + monadInv MAKE. + destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate. + destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate. + exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'. + exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'. + destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate. - destruct s; inv H0; econstructor; eauto with cshm. rewrite iop_ok; auto. rewrite iopu_ok; auto. - destruct s; inv H0; econstructor; eauto with cshm. rewrite lop_ok; auto. rewrite lopu_ok; auto. -- destruct s2; inv H0; econstructor; eauto with cshm. - rewrite lop_ok; auto. rewrite lopu_ok; auto. -- destruct s1; inv H0; econstructor; eauto with cshm. - rewrite lop_ok; auto. rewrite lopu_ok; auto. Qed. End MAKE_BIN. -- cgit