diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 08:19:32 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 08:19:32 +0100 |
commit | 0d471625d7613a72c0bb8519e0427f971b53b35f (patch) | |
tree | 7478569a4118ff0cf851f8d491d628aa78454955 /x86 | |
parent | bc5b28ec16590c52da2772b1cc296247ccf528c1 (diff) | |
parent | 3bdb983e0b21c8d45e85aff08278475396038f4f (diff) | |
download | compcert-kvx-0d471625d7613a72c0bb8519e0427f971b53b35f.tar.gz compcert-kvx-0d471625d7613a72c0bb8519e0427f971b53b35f.zip |
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'x86')
-rw-r--r-- | x86/Asmexpand.ml | 2 | ||||
-rw-r--r-- | x86/Builtins1.v | 4 | ||||
-rw-r--r-- | x86/Conventions1.v | 44 |
3 files changed, 31 insertions, 19 deletions
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 35d555f9..ab4c4b13 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -100,22 +100,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 := @@ -127,8 +125,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 *) @@ -138,7 +136,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. *) @@ -148,14 +146,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. @@ -164,7 +162,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. @@ -474,3 +472,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. |