diff options
Diffstat (limited to 'backend/SplitLong.vp')
| -rw-r--r-- | backend/SplitLong.vp | 36 |
1 files changed, 4 insertions, 32 deletions
diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index 694bb0e2..0f240602 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -10,47 +10,19 @@ (* *) (* *********************************************************************) +(* FIXME: expected branching information not propagated *) (** Instruction selection for 64-bit integer operations *) 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}. @@ -285,7 +257,7 @@ Definition cmpl_ne_zero (e: expr) := Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + Econdition (CEcond (Ccomp Ceq) None (h1:::h2:::Enil)) (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) (Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))). @@ -307,7 +279,7 @@ Definition cmplu (c: comparison) (e1 e2: expr) := Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + Econdition (CEcond (Ccomp Ceq) None (h1:::h2:::Enil)) (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) (Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))). |