diff options
Diffstat (limited to 'backend/SplitLong.vp')
| -rw-r--r-- | backend/SplitLong.vp | 31 |
1 files changed, 1 insertions, 30 deletions
diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index 694bb0e2..dfe42df0 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -16,41 +16,12 @@ Require String. Require Import Coqlib. Require Import AST Integers Floats. Require Import Op CminorSel. +Require Import OpHelpers. 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. *) - -Class helper_functions := mk_helper_functions { - i64_dtos: ident; (**r float64 -> signed long *) - i64_dtou: ident; (**r float64 -> unsigned long *) - i64_stod: ident; (**r signed long -> float64 *) - i64_utod: ident; (**r unsigned long -> float64 *) - i64_stof: ident; (**r signed long -> float32 *) - i64_utof: ident; (**r unsigned long -> float32 *) - i64_sdiv: ident; (**r signed division *) - i64_udiv: ident; (**r unsigned division *) - i64_smod: ident; (**r signed remainder *) - i64_umod: ident; (**r unsigned remainder *) - i64_shl: ident; (**r shift left *) - i64_shr: ident; (**r shift right unsigned *) - i64_sar: ident; (**r shift right signed *) - i64_umulh: ident; (**r unsigned multiply high *) - i64_smulh: ident; (**r signed multiply high *) -}. - -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. - Section SELECT. Context {hf: helper_functions}. |