From be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 18 Feb 2020 16:57:17 +0100 Subject: Refine the type of function results in AST.signature Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions. --- x86/Asmexpand.ml | 2 +- x86/Builtins1.v | 4 ++-- x86/Conventions1.v | 30 ++++++++++++++---------------- 3 files changed, 17 insertions(+), 19 deletions(-) (limited to 'x86') diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml index 16426ce3..c82d406e 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -506,7 +506,7 @@ let expand_instruction instr = (* Save the registers *) emit (Pleaq (R10, linear_addr RSP (Z.of_uint save_regs))); emit (Pcall_s (intern_string "__compcert_va_saveregs", - {sig_args = []; sig_res = None; sig_cc = cc_default})) + {sig_args = []; sig_res = Tvoid; sig_cc = cc_default})) end; (* Stack chaining *) let fullsz = sz + 8 in diff --git a/x86/Builtins1.v b/x86/Builtins1.v index 6103cc4c..f1d60961 100644 --- a/x86/Builtins1.v +++ b/x86/Builtins1.v @@ -33,10 +33,10 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with | BI_fmin | BI_fmax => - mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default + mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default end. -Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with | BI_fmin => mkbuiltin_n2t Tfloat Tfloat Tfloat diff --git a/x86/Conventions1.v b/x86/Conventions1.v index 646c4afb..595cb721 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -99,22 +99,20 @@ Definition is_float_reg (r: mreg) := function with one integer result. *) Definition loc_result_32 (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One AX - | Some (Tint | Tany32) => One AX - | Some (Tfloat | Tsingle) => One FP0 - | Some Tany64 => One X0 - | Some Tlong => Twolong DX AX + match proj_sig_res s with + | Tint | Tany32 => One AX + | Tfloat | Tsingle => One FP0 + | Tany64 => One X0 + | Tlong => Twolong DX AX end. (** In 64 bit mode, he result value of a function is passed back to the caller in registers [AX] or [X0]. *) Definition loc_result_64 (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One AX - | Some (Tint | Tlong | Tany32 | Tany64) => One AX - | Some (Tfloat | Tsingle) => One X0 + match proj_sig_res s with + | Tint | Tlong | Tany32 | Tany64 => One AX + | Tfloat | Tsingle => One X0 end. Definition loc_result := @@ -126,8 +124,8 @@ Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result, loc_result_32, loc_result_64, mreg_type; - destruct Archi.ptr64; destruct (sig_res sig) as [[]|]; auto. + intros. unfold loc_result, loc_result_32, loc_result_64, mreg_type; + destruct Archi.ptr64; destruct (proj_sig_res sig); auto. Qed. (** The result locations are caller-save registers *) @@ -137,7 +135,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. unfold loc_result, loc_result_32, loc_result_64, is_callee_save; - destruct Archi.ptr64; destruct (sig_res s) as [[]|]; simpl; auto. + destruct Archi.ptr64; destruct (proj_sig_res s); simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -147,14 +145,14 @@ Lemma loc_result_pair: match loc_result sg with | One _ => True | Twolong r1 r2 => - r1 <> r2 /\ sg.(sig_res) = Some Tlong + r1 <> r2 /\ proj_sig_res sg = Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.ptr64 = false end. Proof. intros. unfold loc_result, loc_result_32, loc_result_64, mreg_type; - destruct Archi.ptr64; destruct (sig_res sg) as [[]|]; auto. + destruct Archi.ptr64; destruct (proj_sig_res sg); auto. split; auto. congruence. Qed. @@ -163,7 +161,7 @@ Qed. Lemma loc_result_exten: forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. Proof. - intros. unfold loc_result, loc_result_32, loc_result_64. + intros. unfold loc_result, loc_result_32, loc_result_64, proj_sig_res. destruct Archi.ptr64; rewrite H; auto. Qed. -- cgit From 28f235806aa0918499b2ef162110f513ebe4db30 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 19 Feb 2020 12:50:55 +0100 Subject: Support re-normalization of values returned by function calls Some ABIs leave more flexibility concerning function return values than CompCert expects. For example, the x86 ABI says that a function result of type "char" is returned in register AL, leaving the top 24 bits of register EAX unspecified, while CompCert expects EAX to contain 32 valid bits, namely the zero- or sign-extension of the 8-bit result. This commits adds a general mechanism to insert "re-normalization" conversions on the results of function calls. Currently, it only deals with results of small integer types, and inserts zero- or sign-extensions if so instructed by a platform-dependent function, Convention1.return_value_needs_normalization. The conversions in question are inserted early in the front-end, so that they can be optimized away in the back-end. The semantic preservation proof is still conducted against the CompCert model, where the return values of functions are already normalized. What the proof shows is that the extra conversions have no effect in this case. In future work we could relax the CompCert model, allowing functions to return values that are not normalized. --- x86/Conventions1.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'x86') diff --git a/x86/Conventions1.v b/x86/Conventions1.v index 595cb721..01b15e98 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -471,3 +471,17 @@ Lemma loc_arguments_main: Proof. unfold loc_arguments; destruct Archi.ptr64; reflexivity. Qed. + +(** ** Normalization of function results *) + +(** In the x86 ABI, a return value of type "char" is returned in + register AL, leaving the top 24 bits of EAX unspecified. + Likewise, a return value of type "short" is returned in register + AH, leaving the top 16 bits of EAX unspecified. Hence, return + values of small integer types need re-normalization after calls. *) + +Definition return_value_needs_normalization (t: rettype) : bool := + match t with + | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true + | _ => false + end. -- cgit