diff options
Diffstat (limited to 'backend/Selection.v')
| -rw-r--r-- | backend/Selection.v | 57 |
1 files changed, 43 insertions, 14 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index a5bef9ae..8667922f 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -26,7 +26,7 @@ Require String. Require Import Coqlib Maps. Require Import AST Errors Integers Globalenvs Builtins Switch. Require Cminor. -Require Import Op CminorSel Cminortyping. +Require Import Op CminorSel OpHelpers Cminortyping. Require Import SelectOp SplitLong SelectLong SelectDiv. Require Machregs. @@ -35,12 +35,13 @@ Local Open Scope error_monad_scope. (** Conversion of conditions *) -Function condexpr_of_expr (e: expr) : condexpr := +Function condexpr_of_expr (e: expr) (expected : option bool) : condexpr := match e with - | Eop (Ocmp c) el => CEcond c el - | Econdition a b c => CEcondition a (condexpr_of_expr b) (condexpr_of_expr c) - | Elet a b => CElet a (condexpr_of_expr b) - | _ => CEcond (Ccompuimm Cne Int.zero) (e ::: Enil) + | Eop (Ocmp c) el => CEcond c expected el + | Econdition a b c => CEcondition a (condexpr_of_expr b expected) + (condexpr_of_expr c expected) + | Elet a b => CElet a (condexpr_of_expr b expected) + | _ => CEcond (Ccompuimm Cne Int.zero) expected (e ::: Enil) end. Function condition_of_expr (e: expr) : condition * exprlist := @@ -120,6 +121,7 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr := Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := match op with + | Cminor.Oexpect ty => arg1 | Cminor.Oadd => add arg1 arg2 | Cminor.Osub => sub arg1 arg2 | Cminor.Omul => mul arg1 arg2 @@ -166,7 +168,7 @@ Definition sel_select (ty: typ) (cnd ifso ifnot: expr) : expr := let (cond, args) := condition_of_expr cnd in match SelectOp.select ty cond args ifso ifnot with | Some a => a - | None => Econdition (condexpr_of_expr cnd) ifso ifnot + | None => Econdition (condexpr_of_expr cnd None) ifso ifnot end. (** Conversion from Cminor expression to Cminorsel expressions *) @@ -243,7 +245,8 @@ Definition sel_builtin_res (optid: option ident) : builtin_res ident := Function sel_known_builtin (bf: builtin_function) (args: exprlist) := match bf, args with | BI_platform b, _ => - SelectOp.platform_builtin b args + SelectOp.platform_builtin b args +(* | BI_standard BI_expect, a1 ::: a2 ::: Enil => Some a1 *) | BI_standard (BI_select ty), a1 ::: a2 ::: a3 ::: Enil => Some (sel_select ty a1 a2 a3) | BI_standard BI_fabs, a1 ::: Enil => @@ -302,16 +305,16 @@ Fixpoint sel_switch (arg: nat) (t: comptree): exitexpr := | CTaction act => XEexit act | CTifeq key act t' => - XEcondition (condexpr_of_expr (make_cmp_eq (Eletvar arg) key)) + XEcondition (condexpr_of_expr (make_cmp_eq (Eletvar arg) key) None) (XEexit act) (sel_switch arg t') | CTiflt key t1 t2 => - XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar arg) key)) + XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar arg) key) None) (sel_switch arg t1) (sel_switch arg t2) | CTjumptable ofs sz tbl t' => XElet (make_sub (Eletvar arg) ofs) - (XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar O) sz)) + (XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar O) sz) None) (XEjumptable (make_to_int (Eletvar O)) tbl) (sel_switch (S arg) t')) end. @@ -386,6 +389,22 @@ Definition if_conversion | _, _ => None end. +Definition extract_expect1 (e : Cminor.expr) : option bool := + match e with + | Cminor.Ebinop (Cminor.Oexpect ty) e1 (Cminor.Econst (Cminor.Ointconst c)) => + Some (if Int.eq_dec c Int.zero then false else true) + | Cminor.Ebinop (Cminor.Oexpect ty) e1 (Cminor.Econst (Cminor.Olongconst c)) => + Some (if Int64.eq_dec c Int64.zero then false else true) + | _ => None + end. + +Definition extract_expect (e : Cminor.expr) : option bool := + match e with + | Cminor.Ebinop (Cminor.Ocmpu Cne) e1 (Cminor.Econst (Cminor.Ointconst c)) => + if Int.eq_dec c Int.zero then extract_expect1 e1 else None + | _ => extract_expect1 e + end. + (** Conversion from Cminor statements to Cminorsel statements. *) Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt := @@ -413,8 +432,10 @@ Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt : match if_conversion ki env e ifso ifnot with | Some s => OK s | None => - do ifso' <- sel_stmt ki env ifso; do ifnot' <- sel_stmt ki env ifnot; - OK (Sifthenelse (condexpr_of_expr (sel_expr e)) ifso' ifnot') + do ifso' <- sel_stmt ki env ifso; + do ifnot' <- sel_stmt ki env ifnot; + OK (Sifthenelse (condexpr_of_expr (sel_expr e) + (extract_expect e)) ifso' ifnot') end | Cminor.Sloop body => do body' <- sel_stmt ki env body; OK (Sloop body') @@ -518,11 +539,19 @@ Definition get_helpers (defmap: PTree.t globdef) : res helper_functions := do i64_sar <- lookup_helper globs "__compcert_i64_sar" sig_li_l ; do i64_umulh <- lookup_helper globs "__compcert_i64_umulh" sig_ll_l ; do i64_smulh <- lookup_helper globs "__compcert_i64_smulh" sig_ll_l ; + do i32_sdiv <- lookup_helper globs "__compcert_i32_sdiv" sig_ii_i ; + do i32_udiv <- lookup_helper globs "__compcert_i32_udiv" sig_ii_i ; + do i32_smod <- lookup_helper globs "__compcert_i32_smod" sig_ii_i ; + do i32_umod <- lookup_helper globs "__compcert_i32_umod" sig_ii_i ; + do f64_div <- lookup_helper globs "__compcert_f64_div" sig_ff_f ; + do f32_div <- lookup_helper globs "__compcert_f32_div" sig_ss_s ; OK (mk_helper_functions i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof i64_sdiv i64_udiv i64_smod i64_umod i64_shl i64_shr i64_sar - i64_umulh i64_smulh). + i64_umulh i64_smulh + i32_sdiv i32_udiv i32_smod i32_umod + f64_div f32_div). (** Conversion of programs. *) |