Require Recdef.
Require Import FSets.
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Registers.
Require Import Op.
Require Import RTL.
Require Import RTLt.
Require Import Kildall.
Require Import KildallComp.
Require Import Utils.
Require Import Classical.

The cfg predicate

Inductive cfg (code:code) (i j:RTL.node) : Prop :=
  | CFG : forall ins
    (HCFG_ins: code!i = Some ins)
    (HCFG_in : In j (successors_instr ins)),
    cfg code i j.

Inductive cfg_star (code:code) (i:RTL.node) : RTL.node -> Prop :=
| cfg_star0 : cfg_star code i i
| cfg_star1 : forall j k, cfg_star code i j -> cfg code j k -> cfg_star code i k.

Lemma cfg_star_same : forall code i j,
  cfg_star code i j <-> (cfg code)** i j.

Lemma cfg_star_same_code: forall code1 code2 i,
  (forall k, cfg_star code1 i k -> code1!k = code2!k) ->
  forall j, cfg_star code1 i j -> cfg_star code2 i j.


Ltac simpl_succs :=
  match goal with
    | [H1 : (RTL.fn_code ?f) ! ?pc = Some _ |- _ ] =>
      unfold successors_list, RTL.successors_map ; rewrite PTree.gmap1 ;
        (rewrite H1; simpl; auto)
  end.
  

Registers that are used in the code of a RTL function

  Inductive use_rtl_code (f: function) : Registers.reg -> node -> Prop :=
  | UIop: forall pc arg op args dst s,
    (RTLt.fn_code f) !pc = Some (RTL.Iop op args dst s) -> In arg args -> use_rtl_code f arg pc
  | UIload: forall pc arg chk adr args dst s,
    (RTLt.fn_code f) !pc = Some (RTL.Iload chk adr args dst s) -> In arg args -> use_rtl_code f arg pc
  | UIcond: forall pc arg cond args s s',
    (RTLt.fn_code f) !pc = Some (RTL.Icond cond args s s') -> In arg args -> use_rtl_code f arg pc
  | UIbuiltin: forall pc arg ef args dst s,
    (RTLt.fn_code f) !pc = Some (RTL.Ibuiltin ef args dst s) -> In arg (params_of_builtin_args args) -> use_rtl_code f arg pc
  | UIstore: forall pc arg chk adr args src s,
    (RTLt.fn_code f) !pc = Some (RTL.Istore chk adr args src s) -> In arg (src::args) -> use_rtl_code f arg pc
  | UIcall: forall pc arg sig r args dst s,
    (RTLt.fn_code f) !pc = Some (RTL.Icall sig (inl ident r) args dst s) -> In arg (r::args) -> use_rtl_code f arg pc
  | UIcall2: forall pc arg sig id args dst s,
    (RTLt.fn_code f) !pc = Some (RTL.Icall sig (inr _ id) args dst s) -> In arg args -> use_rtl_code f arg pc
  | UItailcall: forall pc arg sig r args,
    (RTLt.fn_code f) !pc = Some (RTL.Itailcall sig (inl ident r) args) -> In arg (r::args) -> use_rtl_code f arg pc
  | UItailcall2: forall pc arg sig id args,
    (RTLt.fn_code f) !pc = Some (RTL.Itailcall sig (inr _ id) args) -> In arg args -> use_rtl_code f arg pc
  | UIjump: forall pc arg tbl,
    (RTLt.fn_code f) !pc = Some (RTL.Ijumptable arg tbl) -> use_rtl_code f arg pc
  | UIret: forall pc arg,
    (RTLt.fn_code f) !pc = Some (RTL.Ireturn (Some arg)) -> use_rtl_code f arg pc.
  
  Lemma rtl_cfg_succs : forall f pc pc',
    cfg (fn_code f) pc pc' ->
    In pc' (RTLt.successors_map f) !!! pc.

  Lemma rtl_cfg_succs_instr : forall f pc ins pc',
    cfg (fn_code f) pc pc' ->
    (fn_code f) ! pc = Some ins ->
    In pc' (RTLt.successors_instr ins).

  Hint Resolve rtl_cfg_succs.
  Hint Resolve rtl_cfg_succs_instr.
  Hint Constructors use_rtl_code.
  Hint Extern 4 (In _ (RTL.successors_instr _)) => simpl successors_instr.
  Hint Constructors cfg.

Lemmas about successors and make_predecessors

Lemma succ_code_incl : forall f1 f2,
  (forall i ins, (RTLt.fn_code f1)!i = Some ins -> (RTLt.fn_code f2)!i = Some ins) ->
  forall i, incl ((RTLt.successors_map f1)!!!i) ((RTLt.successors_map f2)!!!i).

Lemma add_successors_correct_inv:
  forall tolist from pred n s,
  In n (add_successors pred from tolist)!!!s ->
  In n pred!!!s \/ (n = from /\ In s tolist).

Lemma make_predecessors_eq : forall (A: Type) (m1 m2 : PTree.t A) succs,
  (forall i, (m1!i) = (m2!i)) ->
  make_predecessors m1 succs = make_predecessors m2 succs.

Inductive join_point (jp : node) (f : function) : Prop :=
  | jp_cons : forall l,
                 forall (Hpreds : (make_predecessors (fn_code f) successors_instr) ! jp = Some l)
                        (Hl : (List.length l > 1)%nat),
                   join_point jp f.


Section UDEF.

Variable f : function.

Inductive assigned_code_spec (code:code) (pc:node) : reg -> Prop :=
| AIop: forall op args dst succ,
  code!pc = Some (Iop op args dst succ) ->
  assigned_code_spec code pc dst
| AIload: forall chunk addr args dst succ,
  code!pc = Some (Iload chunk addr args dst succ) ->
  assigned_code_spec code pc dst
| AIcall: forall sig fn args dst succ,
  code!pc = Some (Icall sig fn args dst succ) ->
  assigned_code_spec code pc dst
| AIbuiltin: forall fn args dst succ,
  code!pc = Some (Ibuiltin fn args (BR dst) succ) ->
  assigned_code_spec code pc dst.
Hint Constructors assigned_code_spec.

End UDEF.