From 9172338a2b82a93a28fd37c943cc3ab51f9f5e0d Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 24 Aug 2013 06:48:26 +0000 Subject: Forgot to add these two files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2310 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/SelectDiv.v | 248 +++++++++++++++++++++++++ backend/SelectLong.v | 510 +++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 758 insertions(+) create mode 100644 backend/SelectDiv.v create mode 100644 backend/SelectLong.v (limited to 'backend') diff --git a/backend/SelectDiv.v b/backend/SelectDiv.v new file mode 100644 index 0000000..e61a088 --- /dev/null +++ b/backend/SelectDiv.v @@ -0,0 +1,248 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Instruction selection for integer division and modulus *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Op. +Require Import CminorSel. +Require Import SelectOp. + +Open Local Scope cminorsel_scope. + +(** We try to turn divisions by a constant into a multiplication by + a pseudo-inverse of the divisor. The approach is described in +- Torbjörn Granlund, Peter L. Montgomery: "Division by Invariant + Integers using Multiplication". PLDI 1994. +- Henry S. Warren, Jr: "Hacker's Delight". Addison-Wesley. Chapter 10. +*) + +Fixpoint find_div_mul_params (fuel: nat) (nc: Z) (d: Z) (p: Z) : option (Z * Z) := + match fuel with + | O => None + | S fuel' => + let twp := two_p p in + if zlt (nc * (d - twp mod d)) twp + then Some(p - 32, (twp + d - twp mod d) / d) + else find_div_mul_params fuel' nc d (p + 1) + end. + +Definition divs_mul_params (d: Z) : option (Z * Z) := + match find_div_mul_params + Int.wordsize + (Int.half_modulus - Int.half_modulus mod d - 1) + d 32 with + | None => None + | Some(p, m) => + if zlt 0 d + && zlt (two_p (32 + p)) (m * d) + && zle (m * d) (two_p (32 + p) + two_p (p + 1)) + && zle 0 m && zlt m Int.modulus + && zle 0 p && zlt p 32 + then Some(p, m) else None + end. + +Definition divu_mul_params (d: Z) : option (Z * Z) := + match find_div_mul_params + Int.wordsize + (Int.modulus - Int.modulus mod d - 1) + d 32 with + | None => None + | Some(p, m) => + if zlt 0 d + && zle (two_p (32 + p)) (m * d) + && zle (m * d) (two_p (32 + p) + two_p p) + && zle 0 m && zlt m Int.modulus + && zle 0 p && zlt p 32 + then Some(p, m) else None + end. + +Definition divu_mul (p: Z) (m: Z) := + shruimm (Eop Omulhu (Eletvar O ::: Eop (Ointconst (Int.repr m)) Enil ::: Enil)) + (Int.repr p). + +Definition divuimm (e1: expr) (n2: int) := + match Int.is_power2 n2 with + | Some l => shruimm e1 l + | None => + match divu_mul_params (Int.unsigned n2) with + | None => divu_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (divu_mul p m) + end + end. + +(** Original definition: +<< +Nondetfunction divu (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => divuimm e1 n2 + | _ => divu_base e1 e2 + end. +>> +*) + +Inductive divu_cases: forall (e2: expr), Type := + | divu_case1: forall n2, divu_cases (Eop (Ointconst n2) Enil) + | divu_default: forall (e2: expr), divu_cases e2. + +Definition divu_match (e2: expr) := + match e2 as zz1 return divu_cases zz1 with + | Eop (Ointconst n2) Enil => divu_case1 n2 + | e2 => divu_default e2 + end. + +Definition divu (e1: expr) (e2: expr) := + match divu_match e2 with + | divu_case1 n2 => (* Eop (Ointconst n2) Enil *) + divuimm e1 n2 + | divu_default e2 => + divu_base e1 e2 + end. + + +Definition mod_from_div (equo: expr) (n: int) := + Eop Osub (Eletvar O ::: mulimm n equo ::: Enil). + +Definition moduimm (e1: expr) (n2: int) := + match Int.is_power2 n2 with + | Some l => andimm (Int.sub n2 Int.one) e1 + | None => + match divu_mul_params (Int.unsigned n2) with + | None => modu_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2) + end + end. + +(** Original definition: +<< +Nondetfunction modu (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => moduimm e1 n2 + | _ => modu_base e1 e2 + end. +>> +*) + +Inductive modu_cases: forall (e2: expr), Type := + | modu_case1: forall n2, modu_cases (Eop (Ointconst n2) Enil) + | modu_default: forall (e2: expr), modu_cases e2. + +Definition modu_match (e2: expr) := + match e2 as zz1 return modu_cases zz1 with + | Eop (Ointconst n2) Enil => modu_case1 n2 + | e2 => modu_default e2 + end. + +Definition modu (e1: expr) (e2: expr) := + match modu_match e2 with + | modu_case1 n2 => (* Eop (Ointconst n2) Enil *) + moduimm e1 n2 + | modu_default e2 => + modu_base e1 e2 + end. + + +Definition divs_mul (p: Z) (m: Z) := + let e2 := + Eop Omulhs (Eletvar O ::: Eop (Ointconst (Int.repr m)) Enil ::: Enil) in + let e3 := + if zlt m Int.half_modulus then e2 else add e2 (Eletvar O) in + add (shrimm e3 (Int.repr p)) + (shruimm (Eletvar O) (Int.repr (Int.zwordsize - 1))). + +Definition divsimm (e1: expr) (n2: int) := + match Int.is_power2 n2 with + | Some l => + if Int.ltu l (Int.repr 31) + then shrximm e1 l + else divs_base e1 (Eop (Ointconst n2) Enil) + | None => + match divs_mul_params (Int.signed n2) with + | None => divs_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (divs_mul p m) + end + end. + +(** Original definition: +<< +Nondetfunction divs (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => divsimm e1 n2 + | _ => divs_base e1 e2 + end. +>> +*) + +Inductive divs_cases: forall (e2: expr), Type := + | divs_case1: forall n2, divs_cases (Eop (Ointconst n2) Enil) + | divs_default: forall (e2: expr), divs_cases e2. + +Definition divs_match (e2: expr) := + match e2 as zz1 return divs_cases zz1 with + | Eop (Ointconst n2) Enil => divs_case1 n2 + | e2 => divs_default e2 + end. + +Definition divs (e1: expr) (e2: expr) := + match divs_match e2 with + | divs_case1 n2 => (* Eop (Ointconst n2) Enil *) + divsimm e1 n2 + | divs_default e2 => + divs_base e1 e2 + end. + + +Definition modsimm (e1: expr) (n2: int) := + match Int.is_power2 n2 with + | Some l => + if Int.ltu l (Int.repr 31) + then Elet e1 (mod_from_div (shrximm (Eletvar O) l) n2) + else mods_base e1 (Eop (Ointconst n2) Enil) + | None => + match divs_mul_params (Int.signed n2) with + | None => mods_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2) + end + end. + +(** Original definition: +<< +Nondetfunction mods (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => modsimm e1 n2 + | _ => mods_base e1 e2 + end. +>> +*) + +Inductive mods_cases: forall (e2: expr), Type := + | mods_case1: forall n2, mods_cases (Eop (Ointconst n2) Enil) + | mods_default: forall (e2: expr), mods_cases e2. + +Definition mods_match (e2: expr) := + match e2 as zz1 return mods_cases zz1 with + | Eop (Ointconst n2) Enil => mods_case1 n2 + | e2 => mods_default e2 + end. + +Definition mods (e1: expr) (e2: expr) := + match mods_match e2 with + | mods_case1 n2 => (* Eop (Ointconst n2) Enil *) + modsimm e1 n2 + | mods_default e2 => + mods_base e1 e2 + end. + + diff --git a/backend/SelectLong.v b/backend/SelectLong.v new file mode 100644 index 0000000..5ba892d --- /dev/null +++ b/backend/SelectLong.v @@ -0,0 +1,510 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Instruction selection for 64-bit integer operations *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Op. +Require Import CminorSel. +Require Import SelectOp. + +Open Local Scope cminorsel_scope. + +(** Some operations on 64-bit integers are transformed into calls to + runtime library functions. The following record type collects + the names of these functions. *) + +Record helper_functions : Type := mk_helper_functions { + i64_dtos: ident; (**r float -> signed long *) + i64_dtou: ident; (**r float -> unsigned long *) + i64_stod: ident; (**r signed long -> float *) + i64_utod: ident; (**r unsigned long -> float *) + i64_stof: ident; (**r signed long -> float32 *) + i64_utof: ident; (**r unsigned long -> float32 *) + i64_neg: ident; (**r opposite *) + i64_add: ident; (**r addition *) + i64_sub: ident; (**r subtraction *) + i64_mul: ident; (**r multiplication 32x32->64 *) + 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 *) +}. + +Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong). +Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat). +Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle). +Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong). +Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong). +Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong). +Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong). + +Section SELECT. + +Variable hf: helper_functions. + +Definition makelong (h l: expr): expr := + Eop Omakelong (h ::: l ::: Enil). + +(** Original definition: +<< +Nondetfunction splitlong (e: expr) (f: expr -> expr -> expr) := + match e with + | Eop Omakelong (h ::: l ::: Enil) => f h l + | _ => Elet e (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))) + end. +>> +*) + +Inductive splitlong_cases: forall (e: expr) , Type := + | splitlong_case1: forall h l, splitlong_cases (Eop Omakelong (h ::: l ::: Enil)) + | splitlong_default: forall (e: expr) , splitlong_cases e. + +Definition splitlong_match (e: expr) := + match e as zz1 return splitlong_cases zz1 with + | Eop Omakelong (h ::: l ::: Enil) => splitlong_case1 h l + | e => splitlong_default e + end. + +Definition splitlong (e: expr) (f: expr -> expr -> expr) := + match splitlong_match e with + | splitlong_case1 h l => (* Eop Omakelong (h ::: l ::: Enil) *) + f h l + | splitlong_default e => + Elet e (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))) + end. + + +(** Original definition: +<< +Nondetfunction splitlong2 (e1 e2: expr) (f: expr -> expr -> expr -> expr -> expr) := + match e1, e2 with + | Eop Omakelong (h1 ::: l1 ::: Enil), Eop Omakelong (h2 ::: l2 ::: Enil) => + f h1 l1 h2 l2 + | Eop Omakelong (h1 ::: l1 ::: Enil), t2 => + Elet t2 (f (lift h1) (lift l1) + (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))) + | t1, Eop Omakelong (h2 ::: l2 ::: Enil) => + Elet t1 (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)) + (lift h2) (lift l2)) + | _, _ => + Elet e1 (Elet (lift e2) + (f (Eop Ohighlong (Eletvar 1 ::: Enil)) (Eop Olowlong (Eletvar 1 ::: Enil)) + (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)))) + end. +>> +*) + +Inductive splitlong2_cases: forall (e1 e2: expr) , Type := + | splitlong2_case1: forall h1 l1 h2 l2, splitlong2_cases (Eop Omakelong (h1 ::: l1 ::: Enil)) (Eop Omakelong (h2 ::: l2 ::: Enil)) + | splitlong2_case2: forall h1 l1 t2, splitlong2_cases (Eop Omakelong (h1 ::: l1 ::: Enil)) (t2) + | splitlong2_case3: forall t1 h2 l2, splitlong2_cases (t1) (Eop Omakelong (h2 ::: l2 ::: Enil)) + | splitlong2_default: forall (e1 e2: expr) , splitlong2_cases e1 e2. + +Definition splitlong2_match (e1 e2: expr) := + match e1 as zz1, e2 as zz2 return splitlong2_cases zz1 zz2 with + | Eop Omakelong (h1 ::: l1 ::: Enil), Eop Omakelong (h2 ::: l2 ::: Enil) => splitlong2_case1 h1 l1 h2 l2 + | Eop Omakelong (h1 ::: l1 ::: Enil), t2 => splitlong2_case2 h1 l1 t2 + | t1, Eop Omakelong (h2 ::: l2 ::: Enil) => splitlong2_case3 t1 h2 l2 + | e1, e2 => splitlong2_default e1 e2 + end. + +Definition splitlong2 (e1 e2: expr) (f: expr -> expr -> expr -> expr -> expr) := + match splitlong2_match e1 e2 with + | splitlong2_case1 h1 l1 h2 l2 => (* Eop Omakelong (h1 ::: l1 ::: Enil), Eop Omakelong (h2 ::: l2 ::: Enil) *) + f h1 l1 h2 l2 + | splitlong2_case2 h1 l1 t2 => (* Eop Omakelong (h1 ::: l1 ::: Enil), t2 *) + Elet t2 (f (lift h1) (lift l1) (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))) + | splitlong2_case3 t1 h2 l2 => (* t1, Eop Omakelong (h2 ::: l2 ::: Enil) *) + Elet t1 (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)) (lift h2) (lift l2)) + | splitlong2_default e1 e2 => + Elet e1 (Elet (lift e2) (f (Eop Ohighlong (Eletvar 1 ::: Enil)) (Eop Olowlong (Eletvar 1 ::: Enil)) (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)))) + end. + + +(** Original definition: +<< +Nondetfunction lowlong (e: expr) := + match e with + | Eop Omakelong (e1 ::: e2 ::: Enil) => e2 + | _ => Eop Olowlong (e ::: Enil) + end. +>> +*) + +Inductive lowlong_cases: forall (e: expr), Type := + | lowlong_case1: forall e1 e2, lowlong_cases (Eop Omakelong (e1 ::: e2 ::: Enil)) + | lowlong_default: forall (e: expr), lowlong_cases e. + +Definition lowlong_match (e: expr) := + match e as zz1 return lowlong_cases zz1 with + | Eop Omakelong (e1 ::: e2 ::: Enil) => lowlong_case1 e1 e2 + | e => lowlong_default e + end. + +Definition lowlong (e: expr) := + match lowlong_match e with + | lowlong_case1 e1 e2 => (* Eop Omakelong (e1 ::: e2 ::: Enil) *) + e2 + | lowlong_default e => + Eop Olowlong (e ::: Enil) + end. + + +(** Original definition: +<< +Nondetfunction highlong (e: expr) := + match e with + | Eop Omakelong (e1 ::: e2 ::: Enil) => e1 + | _ => Eop Ohighlong (e ::: Enil) + end. +>> +*) + +Inductive highlong_cases: forall (e: expr), Type := + | highlong_case1: forall e1 e2, highlong_cases (Eop Omakelong (e1 ::: e2 ::: Enil)) + | highlong_default: forall (e: expr), highlong_cases e. + +Definition highlong_match (e: expr) := + match e as zz1 return highlong_cases zz1 with + | Eop Omakelong (e1 ::: e2 ::: Enil) => highlong_case1 e1 e2 + | e => highlong_default e + end. + +Definition highlong (e: expr) := + match highlong_match e with + | highlong_case1 e1 e2 => (* Eop Omakelong (e1 ::: e2 ::: Enil) *) + e1 + | highlong_default e => + Eop Ohighlong (e ::: Enil) + end. + + +Definition longconst (n: int64) : expr := + makelong (Eop (Ointconst (Int64.hiword n)) Enil) + (Eop (Ointconst (Int64.loword n)) Enil). + +(** Original definition: +<< +Nondetfunction is_longconst (e: expr) := + match e with + | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => + Some(Int64.ofwords h l) + | _ => + None + end. +>> +*) + +Inductive is_longconst_cases: forall (e: expr), Type := + | is_longconst_case1: forall h l, is_longconst_cases (Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil)) + | is_longconst_default: forall (e: expr), is_longconst_cases e. + +Definition is_longconst_match (e: expr) := + match e as zz1 return is_longconst_cases zz1 with + | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => is_longconst_case1 h l + | e => is_longconst_default e + end. + +Definition is_longconst (e: expr) := + match is_longconst_match e with + | is_longconst_case1 h l => (* Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) *) + Some(Int64.ofwords h l) + | is_longconst_default e => + None + end. + + +Definition is_longconst_zero (e: expr) := + match is_longconst e with + | Some n => Int64.eq n Int64.zero + | None => false + end. + +Definition intoflong (e: expr) := lowlong e. + +Definition longofint (e: expr) := + Elet e (makelong (shrimm (Eletvar O) (Int.repr 31)) (Eletvar O)). + +Definition longofintu (e: expr) := + makelong (Eop (Ointconst Int.zero) Enil) e. + +Definition negl (e: expr) := + match is_longconst e with + | Some n => longconst (Int64.neg n) + | None => Ebuiltin (EF_builtin hf.(i64_neg) sig_l_l) (e ::: Enil) + end. + +Definition notl (e: expr) := + splitlong e (fun h l => makelong (notint h) (notint l)). + +Definition longoffloat (arg: expr) := + Eexternal hf.(i64_dtos) sig_f_l (arg ::: Enil). +Definition longuoffloat (arg: expr) := + Eexternal hf.(i64_dtou) sig_f_l (arg ::: Enil). +Definition floatoflong (arg: expr) := + Eexternal hf.(i64_stod) sig_l_f (arg ::: Enil). +Definition floatoflongu (arg: expr) := + Eexternal hf.(i64_utod) sig_l_f (arg ::: Enil). +Definition singleoflong (arg: expr) := + Eexternal hf.(i64_stof) sig_l_s (arg ::: Enil). +Definition singleoflongu (arg: expr) := + Eexternal hf.(i64_utof) sig_l_s (arg ::: Enil). + +Definition andl (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (and h1 h2) (and l1 l2)). + +Definition orl (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (or h1 h2) (or l1 l2)). + +Definition xorl (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (xor h1 h2) (xor l1 l2)). + +Definition shllimm (e1: expr) (n: int) := + if Int.eq n Int.zero then e1 else + if Int.ltu n Int.iwordsize then + splitlong e1 (fun h l => + makelong (or (shlimm h n) (shruimm l (Int.sub Int.iwordsize n))) + (shlimm l n)) + else if Int.ltu n Int64.iwordsize' then + makelong (shlimm (lowlong e1) (Int.sub n Int.iwordsize)) + (Eop (Ointconst Int.zero) Enil) + else + Eexternal hf.(i64_shl) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + +Definition shrluimm (e1: expr) (n: int) := + if Int.eq n Int.zero then e1 else + if Int.ltu n Int.iwordsize then + splitlong e1 (fun h l => + makelong (shruimm h n) + (or (shruimm l n) (shlimm h (Int.sub Int.iwordsize n)))) + else if Int.ltu n Int64.iwordsize' then + makelong (Eop (Ointconst Int.zero) Enil) + (shruimm (highlong e1) (Int.sub n Int.iwordsize)) + else + Eexternal hf.(i64_shr) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + +Definition shrlimm (e1: expr) (n: int) := + if Int.eq n Int.zero then e1 else + if Int.ltu n Int.iwordsize then + splitlong e1 (fun h l => + makelong (shrimm h n) + (or (shruimm l n) (shlimm h (Int.sub Int.iwordsize n)))) + else if Int.ltu n Int64.iwordsize' then + Elet (highlong e1) + (makelong (shrimm (Eletvar 0) (Int.repr 31)) + (shrimm (Eletvar 0) (Int.sub n Int.iwordsize))) + else + Eexternal hf.(i64_sar) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + +Definition is_intconst (e: expr) := + match e with + | Eop (Ointconst n) Enil => Some n + | _ => None + end. + +Definition shll (e1 e2: expr) := + match is_intconst e2 with + | Some n => shllimm e1 n + | None => Eexternal hf.(i64_shl) sig_li_l (e1 ::: e2 ::: Enil) + end. + +Definition shrlu (e1 e2: expr) := + match is_intconst e2 with + | Some n => shrluimm e1 n + | None => Eexternal hf.(i64_shr) sig_li_l (e1 ::: e2 ::: Enil) + end. + +Definition shrl (e1 e2: expr) := + match is_intconst e2 with + | Some n => shrlimm e1 n + | None => Eexternal hf.(i64_sar) sig_li_l (e1 ::: e2 ::: Enil) + end. + +Definition addl (e1 e2: expr) := + let default := Ebuiltin (EF_builtin hf.(i64_add) sig_ll_l) (e1 ::: e2 ::: Enil) in + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => longconst (Int64.add n1 n2) + | Some n1, _ => if Int64.eq n1 Int64.zero then e2 else default + | _, Some n2 => if Int64.eq n2 Int64.zero then e1 else default + | _, _ => default + end. + +Definition subl (e1 e2: expr) := + let default := Ebuiltin (EF_builtin hf.(i64_sub) sig_ll_l) (e1 ::: e2 ::: Enil) in + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => longconst (Int64.sub n1 n2) + | Some n1, _ => if Int64.eq n1 Int64.zero then negl e2 else default + | _, Some n2 => if Int64.eq n2 Int64.zero then e1 else default + | _, _ => default + end. + +Definition mull_base (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => + Elet (Ebuiltin (EF_builtin hf.(i64_mul) sig_ii_l) (l1 ::: l2 ::: Enil)) + (makelong + (add (add (Eop Ohighlong (Eletvar O ::: Enil)) + (mul (lift l1) (lift h2))) + (mul (lift h1) (lift l2))) + (Eop Olowlong (Eletvar O ::: Enil)))). + +Definition mullimm (e: expr) (n: int64) := + if Int64.eq n Int64.zero then longconst Int64.zero else + if Int64.eq n Int64.one then e else + match Int64.is_power2 n with + | Some l => shllimm e (Int.repr (Int64.unsigned l)) + | None => mull_base e (longconst n) + end. + +Definition mull (e1 e2: expr) := + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => longconst (Int64.mul n1 n2) + | Some n1, _ => mullimm e2 n1 + | _, Some n2 => mullimm e1 n2 + | _, _ => mull_base e1 e2 + end. + +Definition binop_long (id: ident) (sem: int64 -> int64 -> int64) (e1 e2: expr) := + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => longconst (sem n1 n2) + | _, _ => Eexternal id sig_ll_l (e1 ::: e2 ::: Enil) + end. + +Definition divl := binop_long hf.(i64_sdiv) Int64.divs. +Definition modl := binop_long hf.(i64_smod) Int64.mods. + +Definition divlu (e1 e2: expr) := + let default := Eexternal hf.(i64_udiv) sig_ll_l (e1 ::: e2 ::: Enil) in + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => longconst (Int64.divu n1 n2) + | _, Some n2 => + match Int64.is_power2 n2 with + | Some l => shrluimm e1 (Int.repr (Int64.unsigned l)) + | None => default + end + | _, _ => default + end. + +Definition modlu (e1 e2: expr) := + let default := Eexternal hf.(i64_umod) sig_ll_l (e1 ::: e2 ::: Enil) in + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => longconst (Int64.modu n1 n2) + | _, Some n2 => + match Int64.is_power2 n2 with + | Some l => andl e1 (longconst (Int64.sub n2 Int64.one)) + | None => default + end + | _, _ => default + end. + +Definition cmpl_eq_zero (e: expr) := + splitlong e (fun h l => comp Ceq (or h l) (Eop (Ointconst Int.zero) Enil)). + +Definition cmpl_ne_zero (e: expr) := + splitlong e (fun h l => comp Cne (or h l) (Eop (Ointconst Int.zero) Enil)). + +Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => + Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) + (Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))). + +Definition cmplu (c: comparison) (e1 e2: expr) := + match c with + | Ceq => + if is_longconst_zero e2 + then cmpl_eq_zero e1 + else cmpl_eq_zero (xorl e1 e2) + | Cne => + if is_longconst_zero e2 + then cmpl_ne_zero e1 + else cmpl_ne_zero (xorl e1 e2) + | Clt => + cmplu_gen Clt Clt e1 e2 + | Cle => + cmplu_gen Clt Cle e1 e2 + | Cgt => + cmplu_gen Cgt Cgt e1 e2 + | Cge => + cmplu_gen Cgt Cge e1 e2 + end. + +Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => + Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) + (Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))). + +Definition cmpl (c: comparison) (e1 e2: expr) := + match c with + | Ceq => + if is_longconst_zero e2 + then cmpl_eq_zero e1 + else cmpl_eq_zero (xorl e1 e2) + | Cne => + if is_longconst_zero e2 + then cmpl_ne_zero e1 + else cmpl_ne_zero (xorl e1 e2) + | Clt => + if is_longconst_zero e2 + then comp Clt (highlong e1) (Eop (Ointconst Int.zero) Enil) + else cmpl_gen Clt Clt e1 e2 + | Cle => + cmpl_gen Clt Cle e1 e2 + | Cgt => + cmpl_gen Cgt Cgt e1 e2 + | Cge => + if is_longconst_zero e2 + then comp Cge (highlong e1) (Eop (Ointconst Int.zero) Enil) + else cmpl_gen Cgt Cge e1 e2 + end. + +End SELECT. + +(** Setting up the helper functions *) + +Require Import Errors. + +Local Open Scope string_scope. +Local Open Scope error_monad_scope. + +Parameter get_helper: Cminor.genv -> String.string -> signature -> res ident. +Parameter get_builtin: String.string -> signature -> res ident. + +Definition get_helpers (ge: Cminor.genv): res helper_functions := + do i64_dtos <- get_helper ge "__i64_dtos" sig_f_l ; + do i64_dtou <- get_helper ge "__i64_dtou" sig_f_l ; + do i64_stod <- get_helper ge "__i64_stod" sig_l_f ; + do i64_utod <- get_helper ge "__i64_utod" sig_l_f ; + do i64_stof <- get_helper ge "__i64_stof" sig_l_s ; + do i64_utof <- get_helper ge "__i64_utof" sig_l_s ; + do i64_neg <- get_builtin "__builtin_negl" sig_l_l ; + do i64_add <- get_builtin "__builtin_addl" sig_ll_l ; + do i64_sub <- get_builtin "__builtin_subl" sig_ll_l ; + do i64_mul <- get_builtin "__builtin_mull" sig_ll_l ; + do i64_sdiv <- get_helper ge "__i64_sdiv" sig_ll_l ; + do i64_udiv <- get_helper ge "__i64_udiv" sig_ll_l ; + do i64_smod <- get_helper ge "__i64_smod" sig_ll_l ; + do i64_umod <- get_helper ge "__i64_umod" sig_ll_l ; + do i64_shl <- get_helper ge "__i64_shl" sig_li_l ; + do i64_shr <- get_helper ge "__i64_shr" sig_li_l ; + do i64_sar <- get_helper ge "__i64_sar" sig_li_l ; + OK (mk_helper_functions + i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof + i64_neg i64_add i64_sub i64_mul i64_sdiv i64_udiv i64_smod i64_umod + i64_shl i64_shr i64_sar). -- cgit v1.2.3