diff options
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Builtins1.v | 12 | ||||
| -rw-r--r-- | mppa_k1c/Conventions1.v | 31 |
2 files changed, 26 insertions, 17 deletions
diff --git a/mppa_k1c/Builtins1.v b/mppa_k1c/Builtins1.v index 6186961f..3b5cd419 100644 --- a/mppa_k1c/Builtins1.v +++ b/mppa_k1c/Builtins1.v @@ -43,18 +43,18 @@ 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 | BI_fminf | BI_fmaxf => - mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default + mksignature (Tsingle :: Tsingle :: nil) Tsingle cc_default | BI_fabsf => - mksignature (Tsingle :: nil) (Some Tsingle) cc_default + mksignature (Tsingle :: nil) Tsingle cc_default | BI_fma => - mksignature (Tfloat :: Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default + mksignature (Tfloat :: Tfloat :: Tfloat :: nil) Tfloat cc_default | BI_fmaf => - mksignature (Tsingle :: Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default + mksignature (Tsingle :: Tsingle :: Tsingle :: nil) Tsingle 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 ExtFloat.min | BI_fmax => mkbuiltin_n2t Tfloat Tfloat Tfloat ExtFloat.max diff --git a/mppa_k1c/Conventions1.v b/mppa_k1c/Conventions1.v index d41f1095..48346a6d 100644 --- a/mppa_k1c/Conventions1.v +++ b/mppa_k1c/Conventions1.v @@ -90,12 +90,17 @@ Definition is_float_reg (r: mreg) := false. returned value. We treat a function without result as a function with one integer result. *) + Definition loc_result (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One R0 - | Some (Tint | Tany32) => One R0 - | Some (Tfloat | Tsingle | Tany64) => One R0 - | Some Tlong => if Archi.ptr64 then One R0 else One R0 + match s.(sig_res) with + | Tvoid => One R0 + | Tint8signed => One R0 + | Tint8unsigned => One R0 + | Tint16signed => One R0 + | Tint16unsigned => One R0 + | Tint | Tany32 => One R0 + | Tfloat | Tsingle | Tany64 => One R0 + | Tlong => if Archi.ptr64 then One R0 else One R0 end. (** The result registers have types compatible with that given in the signature. *) @@ -104,8 +109,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, mreg_type; - destruct (sig_res sig) as [[]|]; auto; destruct Archi.ptr64; auto. + intros. unfold proj_sig_res, loc_result, mreg_type. + destruct (sig_res sig); try destruct Archi.ptr64; simpl; trivial; destruct t; trivial. Qed. (** The result locations are caller-save registers *) @@ -115,7 +120,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. unfold loc_result, is_callee_save; - destruct (sig_res s) as [[]|]; simpl; auto; destruct Archi.ptr64; simpl; auto. + destruct (sig_res s); simpl; auto; try destruct Archi.ptr64; simpl; auto; try destruct t; simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -125,14 +130,15 @@ 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; destruct (sig_res sg) as [[]|]; auto. - unfold mreg_type; destruct Archi.ptr64; auto. + unfold loc_result; destruct (sig_res sg); auto; + unfold mreg_type; try destruct Archi.ptr64; auto; + destruct t; auto. Qed. (** The location of the result depends only on the result part of the signature *) @@ -409,3 +415,6 @@ Lemma loc_arguments_main: Proof. reflexivity. Qed. + + +Definition return_value_needs_normalization (t: rettype) : bool := false. |