Module Intervalprop

Require Import Coqlib Maps Integers Floats Lattice Kildall.
Require Import AST Linking Builtins.
Require Compopts Machregs.
Require Import Op Registers RTL.
Require Import Liveness ZIntervalDomain ZIntervalAOp RTL_ZIntervalAnalysis ZIntervalAnalysis.
Require Import IntervalpropOp.

Inductive ibool_cases : ibool -> Type :=
| Just_true: ibool_cases (Just true)
| Just_false: ibool_cases (Just false)
| Ibool_default: forall i, ibool_cases i.

Definition ibool_cases_of (ib : ibool) :=
  match ib as ib1 return ibool_cases ib1 with
  | Just true => Just_true
  | Just false => Just_false
  | xx => Ibool_default xx
  end.

Definition transf_instr (f: function) (an: PMap.t (option aenv))
                        (pc: node) (instr: instruction) :=
  match an!!pc with
  | None => instr
  | Some ae =>
      match instr with
      | Inop s => Inop s
      | Iop op args res s =>
          let aargs := aregs ae args in
          match const_for_result (eval_static_operation op aargs) with
          | Some op' =>
              Iop op' nil res s
          | None =>
              let (op', args') := op_strength_reduction op args aargs in
              Iop op' args' res s
          end
      | Iload trap chunk addr args dst s =>
          let aargs := aregs ae args in
          let (addr', args') := addr_strength_reduction addr args aargs in
          Iload trap chunk addr' args' dst s
      | Istore chunk addr args src s =>
          let aargs := aregs ae args in
          let (addr', args') := addr_strength_reduction addr args aargs in
          Istore chunk addr' args' src s
      | Icall sig ros args res s =>
          Icall sig ros args res s
      | Itailcall sig ros args =>
          Itailcall sig ros args
      | Ibuiltin ef args res s =>
          Ibuiltin ef args res s
      | Icond cond args s1 s2 i =>
          let aargs := aregs ae args in
          match ibool_cases_of (eval_static_condition cond aargs) with
          | Just_true => Inop s1
          | Just_false => Inop s2
          | Ibool_default _ =>
              let (cond', args') := cond_strength_reduction cond args aargs in
              Icond cond' args' s1 s2 i
          end
      | Ijumptable arg tbl =>
          Ijumptable arg tbl
      | Ireturn r =>
          Ireturn r
      end
  end.

Definition transf_function (f: function) : function :=
  let an := AA.analyze tt f in
  mkfunction
    f.(fn_sig)
    f.(fn_params)
    f.(fn_stacksize)
    (PTree.map (transf_instr f an) f.(fn_code))
    f.(fn_entrypoint).

Definition transf_fundef (fd: fundef) : fundef :=
  AST.transf_fundef transf_function fd.

Definition transf_program (p: program) : program :=
  transform_program transf_fundef p.