Require Import Coqlib Floats Values Memory.
Require Import Integers AST.
Require Import Op Registers.
Require Import BTL.
Require Import BTL_SEtheory.
Require Import BTL_SEsimuref.
Require Import Asmgen Asmgenproof1.
Require Import OptionMonad ImpHCons.
Require Import IntPromotionCommon.
Require Import FunInd.

Import Notations.
Import SvalNotations.
Import PureComparisons.

Local Open Scope option_monad_scope.

Expansions and rewrites of macro-instructions using "fake" symbolic values

Definition make_lfsv_cmp (is_inv: bool) (fsv1 fsv2: sval) : list_sval :=
  let (fsvfirst, fsvsec) := if is_inv then (fsv1, fsv2) else (fsv2, fsv1) in
  let lfsv := fScons fsvfirst fSnil in
  fScons fsvsec lfsv.

Definition make_lfsv_single (fsv: sval) : list_sval :=
  fScons fsv fSnil.

Definition make_optR (is_x0 is_inv: bool) : option oreg :=
  if is_x0 then
    (if is_inv then Some (X0_L)
    else Some (X0_R))
  else None.


Definition is_normal_cmp cmp :=
  match cmp with | Cne => false | _ => true end.

Definition is_inv_cmp_int (cmp: comparison) : bool :=
  match cmp with | Cle | Cgt => true | _ => false end.

Definition is_inv_cmp_float (cmp: comparison) : bool :=
  match cmp with | Cge | Cgt => true | _ => false end.

Definition cond_int32s (cmp: comparison) (lsv: list_sval) (optR: option oreg) :=
  match cmp with
  | Ceq => fSop (OEseqw optR) lsv
  | Cne => fSop (OEsnew optR) lsv
  | Clt | Cgt => fSop (OEsltw optR) lsv
  | Cle | Cge =>
      let fsv := (fSop (OEsltw optR) lsv) in
      let lfsv := make_lfsv_single fsv in
      fSop (OExoriw Int.one) lfsv
  end.

Definition cond_int32u (cmp: comparison) (lsv: list_sval) (optR: option oreg) :=
  match cmp with
  | Ceq => fSop (OEsequw optR) lsv
  | Cne => fSop (OEsneuw optR) lsv
  | Clt | Cgt => fSop (OEsltuw optR) lsv
  | Cle | Cge =>
      let fsv := (fSop (OEsltuw optR) lsv) in
      let lfsv := make_lfsv_single fsv in
      fSop (OExoriw Int.one) lfsv
  end.

Definition cond_int64s (cmp: comparison) (lsv: list_sval) (optR: option oreg) :=
  match cmp with
  | Ceq => fSop (OEseql optR) lsv
  | Cne => fSop (OEsnel optR) lsv
  | Clt | Cgt => fSop (OEsltl optR) lsv
  | Cle | Cge =>
      let fsv := (fSop (OEsltl optR) lsv) in
      let lfsv := make_lfsv_single fsv in
      fSop (OExoriw Int.one) lfsv
  end.

Definition cond_int64u (cmp: comparison) (lsv: list_sval) (optR: option oreg) :=
  match cmp with
  | Ceq => fSop (OEsequl optR) lsv
  | Cne => fSop (OEsneul optR) lsv
  | Clt | Cgt => fSop (OEsltul optR) lsv
  | Cle | Cge =>
      let fsv := (fSop (OEsltul optR) lsv) in
      let lfsv := make_lfsv_single fsv in
      fSop (OExoriw Int.one) lfsv
  end.

Definition cond_float (cmp: comparison) (lsv: list_sval) :=
  match cmp with
  | Ceq | Cne => fSop OEfeqd lsv
  | Clt | Cgt => fSop OEfltd lsv
  | Cle | Cge => fSop OEfled lsv
  end.

Definition cond_single (cmp: comparison) (lsv: list_sval) :=
  match cmp with
  | Ceq | Cne => fSop OEfeqs lsv
  | Clt | Cgt => fSop OEflts lsv
  | Cle | Cge => fSop OEfles lsv
  end.


Definition load_hilo32 (hi lo: int) :=
  if Int.eq lo Int.zero then
    fSop (OEluiw hi) fSnil
  else
    let fsv := fSop (OEluiw hi) fSnil in
    let lfsv := make_lfsv_single fsv in
    fSop (OEaddiw None lo) lfsv.

Definition load_hilo64 (hi lo: int64) :=
  if Int64.eq lo Int64.zero then
    fSop (OEluil hi) fSnil
  else
    let fsv := fSop (OEluil hi) fSnil in
    let lfsv := make_lfsv_single fsv in
    fSop (OEaddil None lo) lfsv.

Definition loadimm32 (n: int) :=
  match make_immed32 n with
  | Imm32_single imm =>
      fSop (OEaddiw (Some X0_R) imm) fSnil
  | Imm32_pair hi lo => load_hilo32 hi lo
  end.

Definition loadimm64 (n: int64) :=
  match make_immed64 n with
  | Imm64_single imm =>
      fSop (OEaddil (Some X0_R) imm) fSnil
  | Imm64_pair hi lo => load_hilo64 hi lo
  | Imm64_large imm => fSop (OEloadli imm) fSnil
  end.

Operations

Definition opimm32 (fsv1: sval) (n: int) (op: operation) (opimm: int -> operation) :=
  match make_immed32 n with
  | Imm32_single imm =>
      let lfsv := make_lfsv_single fsv1 in
      fSop (opimm imm) lfsv
  | Imm32_pair hi lo =>
      let fsv := load_hilo32 hi lo in
      let lfsv := make_lfsv_cmp false fsv1 fsv in
      fSop op lfsv
  end.

Definition opimm64 (fsv1: sval) (n: int64) (op: operation) (opimm: int64 -> operation) :=
  match make_immed64 n with
  | Imm64_single imm =>
      let lfsv := make_lfsv_single fsv1 in
      fSop (opimm imm) lfsv
  | Imm64_pair hi lo =>
      let fsv := load_hilo64 hi lo in
      let lfsv := make_lfsv_cmp false fsv1 fsv in
      fSop op lfsv
  | Imm64_large imm =>
      let fsv := fSop (OEloadli imm) fSnil in
      let lfsv := make_lfsv_cmp false fsv1 fsv in
      fSop op lfsv
  end.

Definition addimm32 (fsv1: sval) (n: int) (or: option oreg) := opimm32 fsv1 n Oadd (OEaddiw or).
Definition andimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oand OEandiw.
Definition orimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oor OEoriw.
Definition xorimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oxor OExoriw.
Definition sltimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n (OEsltw None) OEsltiw.
Definition sltuimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n (OEsltuw None) OEsltiuw.
Definition addimm64 (fsv1: sval) (n: int64) (or: option oreg) := opimm64 fsv1 n Oaddl (OEaddil or).
Definition andimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oandl OEandil.
Definition orimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oorl OEoril.
Definition xorimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oxorl OExoril.
Definition sltimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n (OEsltl None) OEsltil.
Definition sltuimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n (OEsltul None) OEsltiul.

Definition expanse_condimm_int32s (cmp: comparison) (fsv1: sval) (n: int) :=
  let is_inv := is_inv_cmp_int cmp in
  if Int.eq n Int.zero then
    let optR := make_optR true is_inv in
    let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
    cond_int32s cmp lfsv optR
  else
    match cmp with
    | Ceq | Cne =>
        let optR := make_optR true is_inv in
        let fsv := xorimm32 fsv1 n in
        let lfsv := make_lfsv_cmp false fsv fsv in
        cond_int32s cmp lfsv optR
    | Clt => sltimm32 fsv1 n
    | Cle =>
        if Int.eq n (Int.repr Int.max_signed) then
          let fsv := loadimm32 Int.one in
          let lfsv := make_lfsv_cmp false fsv1 fsv in
          fSop (OEmayundef MUint) lfsv
        else sltimm32 fsv1 (Int.add n Int.one)
    | _ =>
        let optR := make_optR false is_inv in
        let fsv := loadimm32 n in
        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
        cond_int32s cmp lfsv optR
    end.

Definition expanse_condimm_int32u (cmp: comparison) (fsv1: sval) (n: int) :=
  let is_inv := is_inv_cmp_int cmp in
  if Int.eq n Int.zero then
    let optR := make_optR true is_inv in
    let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
    cond_int32u cmp lfsv optR
  else
    match cmp with
    | Clt => sltuimm32 fsv1 n
    | _ =>
        let optR := make_optR false is_inv in
        let fsv := loadimm32 n in
        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
        cond_int32u cmp lfsv optR
    end.

Definition expanse_condimm_int64s (cmp: comparison) (fsv1: sval) (n: int64) :=
  let is_inv := is_inv_cmp_int cmp in
  if Int64.eq n Int64.zero then
    let optR := make_optR true is_inv in
    let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
    cond_int64s cmp lfsv optR
  else
    match cmp with
    | Ceq | Cne =>
        let optR := make_optR true is_inv in
        let fsv := xorimm64 fsv1 n in
        let lfsv := make_lfsv_cmp false fsv fsv in
        cond_int64s cmp lfsv optR
    | Clt => sltimm64 fsv1 n
    | Cle =>
        if Int64.eq n (Int64.repr Int64.max_signed) then
          let fsv := loadimm32 Int.one in
          let lfsv := make_lfsv_cmp false fsv1 fsv in
          fSop (OEmayundef MUlong) lfsv
        else sltimm64 fsv1 (Int64.add n Int64.one)
    | _ =>
        let optR := make_optR false is_inv in
        let fsv := loadimm64 n in
        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
        cond_int64s cmp lfsv optR
    end.

Definition expanse_condimm_int64u (cmp: comparison) (fsv1: sval) (n: int64) :=
  let is_inv := is_inv_cmp_int cmp in
  if Int64.eq n Int64.zero then
    let optR := make_optR true is_inv in
    let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
    cond_int64u cmp lfsv optR
  else
    match cmp with
    | Clt => sltuimm64 fsv1 n
    | _ =>
        let optR := make_optR false is_inv in
        let fsv := loadimm64 n in
        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
        cond_int64u cmp lfsv optR
    end.

Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lsv: list_sval) :=
  let normal := is_normal_cmp cmp in
  let normal' := if cnot then negb normal else normal in
  let fsv := fn_cond cmp lsv in
  let lfsv := make_lfsv_single fsv in
  if normal' then fsv else fSop (OExoriw Int.one) lfsv.

Function target_op_expanse (op: operation) (lsv: list sval) :=
  match op, lsv with
  | Ocmp (Ccomp c), sv1 :: sv2 :: nil =>
      let is_inv := is_inv_cmp_int c in
      let optR := make_optR false is_inv in
      let lfsv := make_lfsv_cmp is_inv sv1 sv2 in
      Some (cond_int32s c lfsv optR)
  | Ocmp (Ccompu c), sv1 :: sv2 :: nil =>
      let is_inv := is_inv_cmp_int c in
      let optR := make_optR false is_inv in
      let lfsv := make_lfsv_cmp is_inv sv1 sv2 in
      Some (cond_int32u c lfsv optR)
  | Ocmp (Ccompimm c imm), sv1 :: nil =>
      Some (expanse_condimm_int32s c sv1 imm)
  | Ocmp (Ccompuimm c imm), sv1 :: nil =>
      Some (expanse_condimm_int32u c sv1 imm)
  | Ocmp (Ccompl c), sv1 :: sv2 :: nil =>
      let is_inv := is_inv_cmp_int c in
      let optR := make_optR false is_inv in
      let lfsv := make_lfsv_cmp is_inv sv1 sv2 in
      Some (cond_int64s c lfsv optR)
  | Ocmp (Ccomplu c), sv1 :: sv2 :: nil =>
      let is_inv := is_inv_cmp_int c in
      let optR := make_optR false is_inv in
      let lfsv := make_lfsv_cmp is_inv sv1 sv2 in
      Some (cond_int64u c lfsv optR)
  | Ocmp (Ccomplimm c imm), sv1 :: nil =>
      Some (expanse_condimm_int64s c sv1 imm)
  | Ocmp (Ccompluimm c imm), sv1 :: nil =>
      Some (expanse_condimm_int64u c sv1 imm)
  | Ocmp (Ccompf c), sv1 :: sv2 :: nil =>
      let is_inv := is_inv_cmp_float c in
      let lfsv := make_lfsv_cmp is_inv sv1 sv2 in
      Some (expanse_cond_fp false cond_float c lfsv)
  | Ocmp (Cnotcompf c), sv1 :: sv2 :: nil =>
      let is_inv := is_inv_cmp_float c in
      let lfsv := make_lfsv_cmp is_inv sv1 sv2 in
      Some (expanse_cond_fp true cond_float c lfsv)
  | Ocmp (Ccompfs c), sv1 :: sv2 :: nil =>
      let is_inv := is_inv_cmp_float c in
      let lfsv := make_lfsv_cmp is_inv sv1 sv2 in
      Some (expanse_cond_fp false cond_single c lfsv)
  | Ocmp (Cnotcompfs c), sv1 :: sv2 :: nil =>
      let is_inv := is_inv_cmp_float c in
      let lfsv := make_lfsv_cmp is_inv sv1 sv2 in
       Some (expanse_cond_fp true cond_single c lfsv)
  | Ofloatconst f, nil =>
      let fsv := loadimm64 (Float.to_bits f) in
      let lfsv := make_lfsv_single fsv in
      Some (fSop (Ofloat_of_bits) lfsv)
  | Osingleconst f, nil =>
      let fsv := loadimm32 (Float32.to_bits f) in
      let lfsv := make_lfsv_single fsv in
      Some (fSop (Osingle_of_bits) lfsv)
  | Ointconst n, nil =>
      Some (loadimm32 n)
  | Olongconst n, nil =>
      Some (loadimm64 n)
  | Oaddimm n, sv1 :: nil =>
      Some (addimm32 sv1 n None)
  | Oaddlimm n, sv1 :: nil =>
      Some (addimm64 sv1 n None)
  | Oandimm n, sv1 :: nil =>
      Some (andimm32 sv1 n)
  | Oandlimm n, sv1 :: nil =>
      Some (andimm64 sv1 n)
  | Oorimm n, sv1 :: nil =>
      Some (orimm32 sv1 n)
  | Oorlimm n, sv1 :: nil =>
      Some (orimm64 sv1 n)
  | Oxorimm n, sv1 :: nil =>
      Some (xorimm32 sv1 n)
  | Oxorlimm n, sv1 :: nil =>
      Some (xorimm64 sv1 n)
  | Ocast8signed, sv1 :: nil =>
      let lfsv := make_lfsv_single sv1 in
      let fsv := fSop (Oshlimm (Int.repr 24)) lfsv in
      let hl' := make_lfsv_single fsv in
      Some (fSop (Oshrimm (Int.repr 24)) hl')
  | Ocast16signed, sv1 :: nil =>
      let lfsv := make_lfsv_single sv1 in
      let fsv := fSop (Oshlimm (Int.repr 16)) lfsv in
      let hl' := make_lfsv_single fsv in
      Some (fSop (Oshrimm (Int.repr 16)) hl')
  | Ocast32unsigned, sv1 :: nil =>
      let lfsv := make_lfsv_single sv1 in
      let cast32s_s := fSop Ocast32signed lfsv in
      let cast32s_l := make_lfsv_single cast32s_s in
      let sllil_s := fSop (Oshllimm (Int.repr 32)) cast32s_l in
      let sllil_l := make_lfsv_single sllil_s in
      Some (fSop (Oshrluimm (Int.repr 32)) sllil_l)
  | Oshrximm n, sv1 :: nil =>
      let lfsv := make_lfsv_single sv1 in
      if Int.eq n Int.zero then
        let lhl := make_lfsv_cmp false sv1 sv1 in
        Some (fSop (OEmayundef (MUshrx n)) lhl)
      else
        if Int.eq n Int.one then
          let srliw_s := fSop (Oshruimm (Int.repr 31)) lfsv in
          let srliw_l := make_lfsv_cmp false sv1 srliw_s in
          let addw_s := fSop Oadd srliw_l in
          let addw_l := make_lfsv_single addw_s in
          let sraiw_s := fSop (Oshrimm Int.one) addw_l in
          let sraiw_l := make_lfsv_cmp false sraiw_s sraiw_s in
          Some (fSop (OEmayundef (MUshrx n)) sraiw_l)
        else
          let sraiw_s := fSop (Oshrimm (Int.repr 31)) lfsv in
          let sraiw_l := make_lfsv_single sraiw_s in
          let srliw_s := fSop (Oshruimm (Int.sub Int.iwordsize n)) sraiw_l in
          let srliw_l := make_lfsv_cmp false sv1 srliw_s in
          let addw_s := fSop Oadd srliw_l in
          let addw_l := make_lfsv_single addw_s in
          let sraiw_s' := fSop (Oshrimm n) addw_l in
          let sraiw_l' := make_lfsv_cmp false sraiw_s' sraiw_s' in
          Some (fSop (OEmayundef (MUshrx n)) sraiw_l')
  | Oshrxlimm n, sv1 :: nil =>
      let lfsv := make_lfsv_single sv1 in
      if Int.eq n Int.zero then
        let lhl := make_lfsv_cmp false sv1 sv1 in
        Some (fSop (OEmayundef (MUshrxl n)) lhl)
      else
        if Int.eq n Int.one then
          let srlil_s := fSop (Oshrluimm (Int.repr 63)) lfsv in
          let srlil_l := make_lfsv_cmp false sv1 srlil_s in
          let addl_s := fSop Oaddl srlil_l in
          let addl_l := make_lfsv_single addl_s in
          let srail_s := fSop (Oshrlimm Int.one) addl_l in
          let srail_l := make_lfsv_cmp false srail_s srail_s in
          Some (fSop (OEmayundef (MUshrxl n)) srail_l)
        else
          let srail_s := fSop (Oshrlimm (Int.repr 63)) lfsv in
          let srail_l := make_lfsv_single srail_s in
          let srlil_s := fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) srail_l in
          let srlil_l := make_lfsv_cmp false sv1 srlil_s in
          let addl_s := fSop Oaddl srlil_l in
          let addl_l := make_lfsv_single addl_s in
          let srail_s' := fSop (Oshrlimm n) addl_l in
          let srail_l' := make_lfsv_cmp false srail_s' srail_s' in
          Some (fSop (OEmayundef (MUshrxl n)) srail_l')
  | _, _ => None
  end.

Branches

Definition transl_cbranch_int32s (cmp: comparison) (optR: option oreg) :=
  match cmp with
  | Ceq => CEbeqw optR
  | Cne => CEbnew optR
  | Clt => CEbltw optR
  | Cle => CEbgew optR
  | Cgt => CEbltw optR
  | Cge => CEbgew optR
  end.

Definition transl_cbranch_int32u (cmp: comparison) (optR: option oreg) :=
  match cmp with
  | Ceq => CEbequw optR
  | Cne => CEbneuw optR
  | Clt => CEbltuw optR
  | Cle => CEbgeuw optR
  | Cgt => CEbltuw optR
  | Cge => CEbgeuw optR
  end.

Definition transl_cbranch_int64s (cmp: comparison) (optR: option oreg) :=
  match cmp with
  | Ceq => CEbeql optR
  | Cne => CEbnel optR
  | Clt => CEbltl optR
  | Cle => CEbgel optR
  | Cgt => CEbltl optR
  | Cge => CEbgel optR
  end.

Definition transl_cbranch_int64u (cmp: comparison) (optR: option oreg) :=
  match cmp with
  | Ceq => CEbequl optR
  | Cne => CEbneul optR
  | Clt => CEbltul optR
  | Cle => CEbgeul optR
  | Cgt => CEbltul optR
  | Cge => CEbgeul optR
  end.

Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lfsv: list_sval) : (condition * list_sval) :=
  let normal := is_normal_cmp cmp in
  let normal' := if cnot then negb normal else normal in
  let fsv := fn_cond cmp lfsv in
  let lfsv' := make_lfsv_cmp false fsv fsv in
  if normal' then ((CEbnew (Some X0_R)), lfsv') else ((CEbeqw (Some X0_R)), lfsv').

Function target_cbranch_expanse (cond: condition) (args: list sval) :=
  match cond, args with
  | (Ccomp c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let cond := transl_cbranch_int32s c (make_optR false is_inv) in
      let lfsv := make_lfsv_cmp is_inv a1 a2 in
      Some (cond, lfsv)
  | (Ccompu c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let cond := transl_cbranch_int32u c (make_optR false is_inv) in
      let lfsv := make_lfsv_cmp is_inv a1 a2 in
      Some (cond, lfsv)
  | (Ccompimm c n), (a1 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      (if Int.eq n Int.zero then
        let lfsv := make_lfsv_cmp is_inv a1 a1 in
        let cond := transl_cbranch_int32s c (make_optR true is_inv) in
        Some (cond, lfsv)
      else
        let fsv := loadimm32 n in
        let lfsv := make_lfsv_cmp is_inv a1 fsv in
        let cond := transl_cbranch_int32s c (make_optR false is_inv) in
        Some (cond, lfsv))
  | (Ccompuimm c n), (a1 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      (if Int.eq n Int.zero then
        let lfsv := make_lfsv_cmp is_inv a1 a1 in
        let cond := transl_cbranch_int32u c (make_optR true is_inv) in
        Some (cond, lfsv)
      else
        let fsv := loadimm32 n in
        let lfsv := make_lfsv_cmp is_inv a1 fsv in
        let cond := transl_cbranch_int32u c (make_optR false is_inv) in
         Some (cond, lfsv))
  | (Ccompl c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let cond := transl_cbranch_int64s c (make_optR false is_inv) in
      let lfsv := make_lfsv_cmp is_inv a1 a2 in
      Some (cond, lfsv)
  | (Ccomplu c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let cond := transl_cbranch_int64u c (make_optR false is_inv) in
      let lfsv := make_lfsv_cmp is_inv a1 a2 in
      Some (cond, lfsv)
  | (Ccomplimm c n), (a1 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      (if Int64.eq n Int64.zero then
        let lfsv := make_lfsv_cmp is_inv a1 a1 in
        let cond := transl_cbranch_int64s c (make_optR true is_inv) in
        Some (cond, lfsv)
      else
        let fsv := loadimm64 n in
        let lfsv := make_lfsv_cmp is_inv a1 fsv in
        let cond := transl_cbranch_int64s c (make_optR false is_inv) in
        Some (cond, lfsv))
  | (Ccompluimm c n), (a1 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      (if Int64.eq n Int64.zero then
        let lfsv := make_lfsv_cmp is_inv a1 a1 in
        let cond := transl_cbranch_int64u c (make_optR true is_inv) in
        Some (cond, lfsv)
      else
        let fsv := loadimm64 n in
        let lfsv := make_lfsv_cmp is_inv a1 fsv in
        let cond := transl_cbranch_int64u c (make_optR false is_inv) in
        Some (cond, lfsv))
  | (Ccompf c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_float c in
      let lfsv := make_lfsv_cmp is_inv a1 a2 in
      Some (expanse_cbranch_fp false cond_float c lfsv)
  | (Cnotcompf c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_float c in
      let lfsv := make_lfsv_cmp is_inv a1 a2 in
      Some (expanse_cbranch_fp true cond_float c lfsv)
  | (Ccompfs c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_float c in
      let lfsv := make_lfsv_cmp is_inv a1 a2 in
      Some (expanse_cbranch_fp false cond_single c lfsv)
  | (Cnotcompfs c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_float c in
      let lfsv := make_lfsv_cmp is_inv a1 a2 in
      Some (expanse_cbranch_fp true cond_single c lfsv)
  | _, _ => None
   end.

Affine terms and SR rewrites

Local Open Scope positive_scope.

Declare Scope hashlist_match.
Notation "'[]'" := (Snil _): hashlist_match.
Notation "'[' sv1 ';' sv2 ']'" := (Scons sv1 (Scons sv2 (Snil _) _) _): hashlist_match.

Declare Scope hashlist_full.
Notation "[ \ h ]" := (Snil h): hashlist_full.
Notation "[ sv1 \ h1 ; sv2 \ h2 ; \ h3 ]" := (Scons sv1 (Scons sv2 (Snil h1) h2) h3) (h2 at next level): hashlist_full.

Local Open Scope hashlist_full.

Definition op_aff64_rv := Oaddl.

Function select_op_aff64_rv op :=
  match op with
  | Oaddl => true
  | _ => false
  end.

Function find_subterm_aff64_rv sv :=
  match sv with
  | Sinput true r h => Some (inr r)
  | Sop (Olongconst l) [ \ h1 ] h2 => Some (inl l)
  | _ => None
  end.

Definition find_term_const_aff64_rv sv1 sv2 :=
  match find_subterm_aff64_rv sv1, find_subterm_aff64_rv sv2 with
  | Some (inl l), _ => Some (l, sv2)
  | _, Some (inl l) => Some (l, sv1)
  | _, _ => None
  end.

Function find_mul_aff64_rv sv :=
  match sv with
  | Sop Omull [ sv1 \ h1 ; sv2 \ h2; \ h3 ] h4 =>
      find_term_const_aff64_rv sv1 sv2
  | _ => None
  end.

Definition build_const_aff64_rv l := fSop (Olongconst l) fSnil.
Definition build_mul_aff64_rv sv1 sv2 := fSop Omull (make_lfsv_cmp false sv1 sv2).
Definition build_flsv_single sv := fScons sv fSnil.

Definition scale_aff64_rv l1 sv :=
  match find_mul_aff64_rv sv with
  | Some (l2, sv') =>
      let const := build_const_aff64_rv (Int64.mul l1 l2) in
      build_mul_aff64_rv const sv'
  | None =>
      match find_subterm_aff64_rv sv with
      | Some (inl l2) =>
          build_const_aff64_rv (Int64.mul l1 l2)
      | _ =>
          let const := build_const_aff64_rv l1 in
          build_mul_aff64_rv const sv
      end
  end.

Function is_aff64_rv sv :=
  match sv with
  | Sfoldr op l sv0 h =>
      if select_op_aff64_rv op then Some ((Oaddl, l), sv0)
      else None
  | _ => None
  end.

Definition merge_aff64_rv sv1 sv2 :=
  match find_mul_aff64_rv sv1, find_mul_aff64_rv sv2 with
  | Some (l1, sv1), Some (l2, sv2) =>
      let const := build_const_aff64_rv (Int64.add l1 l2) in
      Some (build_mul_aff64_rv const sv1)
  | Some (l, sv), None
  | None, Some (l, sv) =>
      let const := build_const_aff64_rv (Int64.add Int64.one l) in
      Some (build_mul_aff64_rv const sv)
  | _, _ => match find_subterm_aff64_rv sv1 with
            | Some (inr _) =>
                let const := build_const_aff64_rv (Int64.repr 2) in
                Some (build_mul_aff64_rv const sv1)
            | _ => None
            end
  end.

Definition acc0_aff64_rv sv1 sv2 :=
  match find_subterm_aff64_rv sv1, find_subterm_aff64_rv sv2 with
  | Some (inl l1), Some (inl l2) => build_const_aff64_rv (Int64.add l1 l2)
  | _, _ => fSop op_aff64_rv (make_lfsv_cmp false sv1 sv2)
  end.

Definition compare_aff64_rv sv1 sv2 :=
  match find_mul_aff64_rv sv1, find_mul_aff64_rv sv2 with
  | Some (l1, sv1), Some (l2, sv2) => fast_cmp sval_get_hid sv1 sv2
  | Some (l, sv), None => fast_cmp sval_get_hid sv sv2
  | None, Some (l, sv) => fast_cmp sval_get_hid sv sv1
  | _, _ => fast_cmp sval_get_hid sv1 sv2
  end.

Declare Scope sum_type_scope.

Notation "'INL' X <- A 'IN' B" := (match A with inl X => B | inr _ => None end)
         (at level 200, X name, A at level 100, B at level 200)
         : sum_type_scope.

Local Open Scope sum_type_scope.

Definition foldrof_aff64_rv sv: (operation * list_sval * sval) :=
  match is_aff64_rv sv with
  | Some (op, lsv, sv0) => (op, lsv, sv0)
  | None =>
      match find_subterm_aff64_rv sv with
      | Some (inl l) => (op_aff64_rv, fSnil, build_const_aff64_rv l)
      | _ =>
          let lsv := build_flsv_single sv in
          (op_aff64_rv, lsv, build_const_aff64_rv Int64.zero)
      end
  end.

Local Open Scope lazy_bool_scope.

Definition add_foldr_aff64_rv sv1 sv2 :=
  let (t1, sv0_1) := foldrof_aff64_rv sv1 in let (op1, lsv1) := t1 in
  let (t2, sv0_2) := foldrof_aff64_rv sv2 in let (op2, lsv2) := t2 in
  if eq_operation op1 op2 &&& select_op_aff64_rv op1 then
    let lsv := merge merge_aff64_rv compare_aff64_rv lsv1 lsv2 in
    SOME s_l1_sv <- find_subterm_aff64_rv sv0_1 IN
    SOME s_l2_sv <- find_subterm_aff64_rv sv0_2 IN
    INL l1 <- s_l1_sv IN INL l2 <- s_l2_sv IN
    let const := build_const_aff64_rv (Int64.add l1 l2) in
    Some (fSfoldr op1 lsv const)
  else None.




Definition op_strength_reduction (op: operation) (lsv: list sval) :=
  match op, lsv with
  | Oshllimm n, sv :: nil =>
      if negb (Int.ltu n Int64.iwordsize') then None else
      let l := Int64.shl' Int64.one n in
      Some (rescale select_op_aff64_rv (scale_aff64_rv l) sv)
  | Oaddlimm l, sv :: nil =>
      let const := build_const_aff64_rv l in
      add_foldr_aff64_rv const sv
  | Oaddl, sv1 :: sv2 :: nil =>
      add_foldr_aff64_rv sv1 sv2
  | Omull, sv1 :: sv2 :: nil =>
      SOME l_sv <- find_term_const_aff64_rv sv1 sv2 IN
      let (l, sv) := l_sv in
      Some (rescale select_op_aff64_rv (scale_aff64_rv l) sv)
  | _, _ => None
  end.

Local Close Scope positive_scope.

Promotions rewrites

Definition promote_sval (sgn : bool) (sv : sval) : sval :=
  fSop (if sgn then Ocast32signed else Ocast32unsigned) (fScons sv fSnil).

Definition promote_svalb (sgn : bool) (sv : sval) (b : bool) : sval :=
  if b then promote_sval sgn sv else sv.

Definition ok_cast_sgn (sgn ceq sgn' : bool) : bool :=
  ceq || bool_eq sgn' sgn.

Definition unpromote_arg (sgn ceq : bool) (arg : sval) (prom : bool) : option sval :=
  if prom
  then match arg with
       | Sop Ocast32unsigned (Scons arg (Snil _) _) _ => ASSERT (ok_cast_sgn sgn ceq false) IN Some arg
       | Sop Ocast32signed (Scons arg (Snil _) _) _ => ASSERT (ok_cast_sgn sgn ceq true) IN Some arg
       | _ => None
       end
  else Some arg.

Fixpoint unpromote_args (sgn : bool) (args : list sval) (pargs : list bool) (cargs : list bool)
  : option (list_sval) :=
  match args, pargs, cargs with
  | nil, nil, nil => Some fSnil
  | arg :: args, prom :: pargs, ceq :: cargs =>
      SOME r0 <- unpromote_arg sgn ceq arg prom IN
      SOME rs <- unpromote_args sgn args pargs cargs IN
      Some (fScons r0 rs)
  | _, _, _ => None
  end.

Definition unpromote_op (op : operation) (args : list sval) (iinfo : option inst_info):
  option (sval * list okclause) :=
  SOME iinfo <- iinfo IN
  match iinfo.(inst_promotion) with
  | IPromotedOp op0 prom sgn ret_sgn =>
      SOME op' <- op_prom_sgb sgn prom IN
      ASSERT (eq_operation op' op) IN
      ASSERT (ok_cast_sgn sgn prom.(op_prom_res_eq) ret_sgn) IN
      SOME args0 <- unpromote_args sgn args
                        prom.(op_prom_args) prom.(op_prom_args_eq) IN
      let sv0 := fSop op0 args0 in
      let okc := fOKpromotableOp op0 prom args0 in
      Some (promote_svalb ret_sgn sv0 prom.(op_prom_res), okc :: nil)
  | _ => None
  end.

Definition unpromote_condition (cond : condition) (args : list sval) (iinfo : inst_info)
  : option (condition * list_sval * list okclause) :=
  match iinfo.(inst_promotion) with
  | IPromotedCond cond0 prom sgn =>
      SOME cond' <- cond_prom_sgb sgn prom IN
      ASSERT (eq_condition cond' cond) IN
      SOME args0 <- unpromote_args sgn args
                        (map (fun _ => true) args) prom.(cond_prom_args_eq) IN
      let okc := fOKpromotableCond cond0 prom args0 in
      Some (cond0, args0, okc :: nil)
  | _ => None
  end.

Choosing what to do according to rewriting rules set

Definition rewrite_ops (RRULES: rrules_set) (op: operation) (lsv: list sval) (iinfo : option inst_info):
  option (sval * list okclause) :=
  match RRULES with
  | RRexpansions => SOME sv <- target_op_expanse op lsv IN
                    Some (sv, nil)
  | RRlct true _ => SOME sv <- op_strength_reduction op lsv IN
                    Some (sv, nil)
  | RRpromotion => unpromote_op op lsv iinfo
  | _ => None
  end.

Definition rewrite_cbranches (RRULES: rrules_set)
  (cond: condition) (args: list sval) (iinfo : inst_info) : option (condition * list_sval * list okclause) :=
  match RRULES with
  | RRexpansions =>
      match target_cbranch_expanse cond args with
      | Some (cond', args') => Some (cond', args', nil)
      | None => None
      end
  | RRpromotion => unpromote_condition cond args iinfo
  | _ => None
  end.

Branch pruning

Local Open Scope impure_scope.

Function type_of_inequality cond: option typ :=
  match cond with
  | Ccompu Cne | Ccomplu Cne
  | Ccompf Cne | Cnotcompf Ceq | Ccompfs Cne | Cnotcompfs Ceq =>
      match type_of_condition cond with
      | ty :: l => Some ty
      | _ => None
      end
  | _ => None
  end.

Function prunable_inequality cond sv: bool :=
  match sv with
  | Sop (Owelldef ty1) (Scons (Sload _ NOTRAP _ _ _ _) (Snil _) _) _=>
      match type_of_inequality cond with
      | Some ty2 => subtype ty1 ty2
      | None => false
      end
  | _ => false
  end.

Definition branch_pruning cond lsv: ?? (option bool) :=
  match lsv_len_two lsv with
  | Some (sv1, sv2) =>
      DO b <~ phys_eq sv1 sv2;;
      if bool_eq b true then
        if prunable_inequality cond sv1 then RET (Some false)
        else RET None
      else RET None
  | None => RET None
  end.