diff options
| -rw-r--r-- | backend/OpHelpers.v | 20 | ||||
| -rw-r--r-- | backend/SplitLong.vp | 2 | ||||
| -rw-r--r-- | mppa_k1c/Builtins1.v | 12 | ||||
| -rw-r--r-- | mppa_k1c/Conventions1.v | 3 |
4 files changed, 21 insertions, 16 deletions
diff --git a/backend/OpHelpers.v b/backend/OpHelpers.v index 53414dab..b9b97903 100644 --- a/backend/OpHelpers.v +++ b/backend/OpHelpers.v @@ -6,16 +6,16 @@ Require Import Op CminorSel. runtime library functions. The following type class collects the names of these functions. *) -Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. -Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default. -Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default. -Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default. -Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default. -Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default. -Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default. -Definition sig_ii_i := mksignature (Tint :: Tint :: nil) (Some Tint) cc_default. -Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default. -Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default. +Definition sig_l_l := mksignature (Tlong :: nil) Tlong cc_default. +Definition sig_l_f := mksignature (Tlong :: nil) Tfloat cc_default. +Definition sig_l_s := mksignature (Tlong :: nil) Tsingle cc_default. +Definition sig_f_l := mksignature (Tfloat :: nil) Tlong cc_default. +Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) Tlong cc_default. +Definition sig_li_l := mksignature (Tlong :: Tint :: nil) Tlong cc_default. +Definition sig_ii_l := mksignature (Tint :: Tint :: nil) Tlong cc_default. +Definition sig_ii_i := mksignature (Tint :: Tint :: nil) Tint cc_default. +Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default. +Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) Tsingle cc_default. Class helper_functions := mk_helper_functions { i64_dtos: ident; (**r float64 -> signed long *) diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index 73e22b98..4464bcdb 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -22,6 +22,7 @@ Require Import SelectOp. Local Open Scope cminorsel_scope. Local Open Scope string_scope. +(* (** Some operations on 64-bit integers are transformed into calls to runtime library functions. The following type class collects the names of these functions. *) @@ -51,6 +52,7 @@ Definition sig_f_l := mksignature (Tfloat :: nil) Tlong cc_default. Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) Tlong cc_default. Definition sig_li_l := mksignature (Tlong :: Tint :: nil) Tlong cc_default. Definition sig_ii_l := mksignature (Tint :: Tint :: nil) Tlong cc_default. +*) Section SELECT. 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 9e9bae6f..ac2117d0 100644 --- a/mppa_k1c/Conventions1.v +++ b/mppa_k1c/Conventions1.v @@ -415,3 +415,6 @@ Lemma loc_arguments_main: Proof. reflexivity. Qed. + + +Definition return_value_needs_normalization (t: rettype) : bool := false. |