Require Import FSets.
Require Import Coqlib.
Require Import Ordered.
Require Import Maps.
Require Import Iteration.
Require Import AST.
Require Import Errors.
Require Import Integers.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Events.
Require Import Smallstep.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import Unusedglob.

Module ISF := FSetFacts.Facts(IS).
Module ISP := FSetProperties.Properties(IS).

Properties of the analysis

Inductive workset_incl (w1 w2: workset) : Prop :=
  workset_incl_intro:
    forall (SEEN: IS.Subset w1.(w_seen) w2.(w_seen))
           (TODO: List.incl w1.(w_todo) w2.(w_todo))
           (TRACK: forall id, IS.In id w2.(w_seen) ->
                      IS.In id w1.(w_seen) \/ List.In id w2.(w_todo)),
    workset_incl w1 w2.

Lemma seen_workset_incl:
  forall w1 w2 id, workset_incl w1 w2 -> IS.In id w1 -> IS.In id w2.

Lemma workset_incl_refl: forall w, workset_incl w w.

Lemma workset_incl_trans:
  forall w1 w2 w3, workset_incl w1 w2 -> workset_incl w2 w3 -> workset_incl w1 w3.

Lemma add_workset_incl:
  forall id w, workset_incl w (add_workset id w).

Lemma addlist_workset_incl:
  forall l w, workset_incl w (addlist_workset l w).

Lemma add_ref_function_incl:
  forall f w, workset_incl w (add_ref_function f w).

Lemma add_ref_globvar_incl:
  forall gv w, workset_incl w (add_ref_globvar gv w).

Lemma add_ref_definition_incl:
  forall pm id w, workset_incl w (add_ref_definition pm id w).

Lemma initial_workset_incl:
  forall p, workset_incl {| w_seen := IS.empty; w_todo := nil |} (initial_workset p).


Lemma seen_add_workset:
  forall id (w: workset), IS.In id (add_workset id w).

Lemma seen_addlist_workset:
  forall id l (w: workset),
  In id l -> IS.In id (addlist_workset l w).

Definition ref_function (f: function) (id: ident) : Prop :=
  exists pc i, f.(fn_code)!pc = Some i /\ In id (ref_instruction i).

Lemma seen_add_ref_function:
  forall id f w,
  ref_function f id -> IS.In id (add_ref_function f w).

Definition ref_fundef (fd: fundef) (id: ident) : Prop :=
  match fd with Internal f => ref_function f id | External ef => False end.

Definition ref_def (gd: globdef fundef unit) (id: ident) : Prop :=
  match gd with
  | Gfun fd => ref_fundef fd id
  | Gvar gv => exists ofs, List.In (Init_addrof id ofs) gv.(gvar_init)
  end.

Lemma seen_add_ref_definition:
  forall pm id gd id' w,
  pm!id = Some gd -> ref_def gd id' -> IS.In id' (add_ref_definition pm id w).

Lemma seen_main_initial_workset:
  forall p, IS.In p.(prog_main) (initial_workset p).

Lemma seen_public_initial_workset:
  forall p id, In id p.(prog_public) -> IS.In id (initial_workset p).

Semantic preservation

Section SOUNDNESS.
Variable p: program.
Variable tp: program.
Hypothesis TRANSF: transform_program p = OK tp.
Let ge := Genv.globalenv p.
Let tge := Genv.globalenv tp.

Let pm := program_map p.



Definition workset_invariant (w: workset) : Prop :=
  forall id gd id',
  IS.In id w -> ~List.In id (w_todo w) -> pm!id = Some gd -> ref_def gd id' ->
  IS.In id' w.

Definition used_set_closed (u: IS.t) : Prop :=
  forall id gd id',
  IS.In id u -> pm!id = Some gd -> ref_def gd id' -> IS.In id' u.

Lemma iter_step_invariant:
  forall w,
  workset_invariant w ->
  match iter_step pm w with
  | inl u => used_set_closed u
  | inr w' => workset_invariant w'
  end.

Theorem used_globals_sound:
  forall u, used_globals p = Some u -> used_set_closed u.

Theorem used_globals_incl:
  forall u, used_globals p = Some u -> IS.Subset (initial_workset p) u.

Definition used: IS.t :=
  match used_globals p with Some u => u | None => IS.empty end.

Remark USED_GLOBALS: used_globals p = Some used.

Definition kept (id: ident) : Prop := IS.In id used.

Theorem kept_closed:
  forall id gd id',
  kept id -> pm!id = Some gd -> ref_def gd id' -> kept id'.

Theorem kept_main:
  kept p.(prog_main).

Theorem kept_public:
  forall id, In id p.(prog_public) -> kept id.

Remark filter_globdefs_accu:
  forall defs accu1 accu2 u,
  filter_globdefs u (accu1 ++ accu2) defs = filter_globdefs u accu1 defs ++ accu2.

Remark filter_globdefs_nil:
  forall u accu defs,
  filter_globdefs u accu defs = filter_globdefs u nil defs ++ accu.

Theorem transform_program_charact:
  forall id, (program_map tp)!id = if IS.mem id used then pm!id else None.


Definition genv_progmap_match (ge: genv) (pm: prog_map) : Prop :=
  forall id,
  match Genv.find_symbol ge id with
  | None => pm!id = None
  | Some b =>
      match pm!id with
      | None => False
      | Some (Gfun fd) => Genv.find_funct_ptr ge b = Some fd
      | Some (Gvar gv) => Genv.find_var_info ge b = Some gv
      end
  end.

Lemma genv_program_map:
  forall p, genv_progmap_match (Genv.globalenv p) (program_map p).

Lemma transform_program_kept:
  forall id b, Genv.find_symbol tge id = Some b -> kept id.


Record meminj_preserves_globals (f: meminj) : Prop := {
  symbols_inject_1: forall id b b' delta,
    f b = Some(b', delta) -> Genv.find_symbol ge id = Some b ->
    delta = 0 /\ Genv.find_symbol tge id = Some b';
  symbols_inject_2: forall id b,
    kept id -> Genv.find_symbol ge id = Some b ->
    exists b', Genv.find_symbol tge id = Some b' /\ f b = Some(b', 0);
  symbols_inject_3: forall id b',
    Genv.find_symbol tge id = Some b' ->
    exists b, Genv.find_symbol ge id = Some b /\ f b = Some(b', 0);
  funct_ptr_inject: forall b b' delta fd,
    f b = Some(b', delta) -> Genv.find_funct_ptr ge b = Some fd ->
    Genv.find_funct_ptr tge b' = Some fd /\ delta = 0 /\
    (forall id, ref_fundef fd id -> kept id);
  var_info_inject: forall b b' delta gv,
    f b = Some(b', delta) -> Genv.find_var_info ge b = Some gv ->
    Genv.find_var_info tge b' = Some gv /\ delta = 0;
  var_info_rev_inject: forall b b' delta gv,
    f b = Some(b', delta) -> Genv.find_var_info tge b' = Some gv ->
    Genv.find_var_info ge b = Some gv /\ delta = 0
}.

Definition init_meminj : meminj :=
  fun b =>
    match Genv.invert_symbol ge b with
    | Some id =>
        match Genv.find_symbol tge id with
        | Some b' => Some (b', 0)
        | None => None
        end
    | None => None
    end.

Remark init_meminj_invert:
  forall b b' delta,
  init_meminj b = Some(b', delta) ->
  delta = 0 /\ exists id, Genv.find_symbol ge id = Some b /\ Genv.find_symbol tge id = Some b'.

Lemma init_meminj_preserves_globals:
  meminj_preserves_globals init_meminj.

Lemma globals_symbols_inject:
  forall j, meminj_preserves_globals j -> symbols_inject j ge tge.

Lemma symbol_address_inject:
  forall j id ofs,
  meminj_preserves_globals j -> kept id ->
  Val.inject j (Genv.symbol_address ge id ofs) (Genv.symbol_address tge id ofs).


Definition regset_inject (f: meminj) (rs rs': regset): Prop :=
  forall r, Val.inject f rs#r rs'#r.

Lemma regs_inject:
  forall f rs rs', regset_inject f rs rs' -> forall l, Val.inject_list f rs##l rs'##l.

Lemma set_reg_inject:
  forall f rs rs' r v v',
  regset_inject f rs rs' -> Val.inject f v v' ->
  regset_inject f (rs#r <- v) (rs'#r <- v').

Lemma set_res_inject:
  forall f rs rs' res v v',
  regset_inject f rs rs' -> Val.inject f v v' ->
  regset_inject f (regmap_setres res v rs) (regmap_setres res v' rs').

Lemma regset_inject_incr:
  forall f f' rs rs', regset_inject f rs rs' -> inject_incr f f' -> regset_inject f' rs rs'.

Lemma regset_undef_inject:
  forall f, regset_inject f (Regmap.init Vundef) (Regmap.init Vundef).

Lemma init_regs_inject:
  forall f args args', Val.inject_list f args args' ->
  forall params,
  regset_inject f (init_regs args params) (init_regs args' params).

Inductive match_stacks (j: meminj):
        list stackframe -> list stackframe -> block -> block -> Prop :=
  | match_stacks_nil: forall bound tbound,
      meminj_preserves_globals j ->
      Ple (Genv.genv_next ge) bound -> Ple (Genv.genv_next tge) tbound ->
      match_stacks j nil nil bound tbound
  | match_stacks_cons: forall res f sp pc rs s tsp trs ts bound tbound
         (STACKS: match_stacks j s ts sp tsp)
         (KEPT: forall id, ref_function f id -> kept id)
         (SPINJ: j sp = Some(tsp, 0))
         (REGINJ: regset_inject j rs trs)
         (BELOW: Plt sp bound)
         (TBELOW: Plt tsp tbound),
      match_stacks j (Stackframe res f (Vptr sp Int.zero) pc rs :: s)
                     (Stackframe res f (Vptr tsp Int.zero) pc trs :: ts)
                     bound tbound.

Lemma match_stacks_preserves_globals:
  forall j s ts bound tbound,
  match_stacks j s ts bound tbound ->
  meminj_preserves_globals j.

Lemma match_stacks_incr:
  forall j j', inject_incr j j' ->
  forall s ts bound tbound, match_stacks j s ts bound tbound ->
  (forall b1 b2 delta,
      j b1 = None -> j' b1 = Some(b2, delta) -> Ple bound b1 /\ Ple tbound b2) ->
  match_stacks j' s ts bound tbound.

Lemma match_stacks_bound:
  forall j s ts bound tbound bound' tbound',
  match_stacks j s ts bound tbound ->
  Ple bound bound' -> Ple tbound tbound' ->
  match_stacks j s ts bound' tbound'.

Inductive match_states: state -> state -> Prop :=
  | match_states_regular: forall s f sp pc rs m ts tsp trs tm j
         (STACKS: match_stacks j s ts sp tsp)
         (KEPT: forall id, ref_function f id -> kept id)
         (SPINJ: j sp = Some(tsp, 0))
         (REGINJ: regset_inject j rs trs)
         (MEMINJ: Mem.inject j m tm),
      match_states (State s f (Vptr sp Int.zero) pc rs m)
                   (State ts f (Vptr tsp Int.zero) pc trs tm)
  | match_states_call: forall s fd args m ts targs tm j
         (STACKS: match_stacks j s ts (Mem.nextblock m) (Mem.nextblock tm))
         (KEPT: forall id, ref_fundef fd id -> kept id)
         (ARGINJ: Val.inject_list j args targs)
         (MEMINJ: Mem.inject j m tm),
      match_states (Callstate s fd args m)
                   (Callstate ts fd targs tm)
  | match_states_return: forall s res m ts tres tm j
         (STACKS: match_stacks j s ts (Mem.nextblock m) (Mem.nextblock tm))
         (RESINJ: Val.inject j res tres)
         (MEMINJ: Mem.inject j m tm),
      match_states (Returnstate s res m)
                   (Returnstate ts tres tm).

Lemma external_call_inject:
  forall ef vargs m1 t vres m2 f m1' vargs',
  meminj_preserves_globals f ->
  external_call ef ge vargs m1 t vres m2 ->
  Mem.inject f m1 m1' ->
  Val.inject_list f vargs vargs' ->
  exists f', exists vres', exists m2',
    external_call ef tge vargs' m1' t vres' m2'
    /\ Val.inject f' vres vres'
    /\ Mem.inject f' m2 m2'
    /\ Mem.unchanged_on (loc_unmapped f) m1 m2
    /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'
    /\ inject_incr f f'
    /\ inject_separated f f' m1 m1'.

Lemma find_function_inject:
  forall j ros rs fd trs,
  meminj_preserves_globals j ->
  find_function ge ros rs = Some fd ->
  match ros with inl r => regset_inject j rs trs | inr id => kept id end ->
  find_function tge ros trs = Some fd /\ (forall id, ref_fundef fd id -> kept id).

Lemma eval_builtin_arg_inject:
  forall rs sp m j rs' sp' m' a v,
  eval_builtin_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v ->
  j sp = Some(sp', 0) ->
  meminj_preserves_globals j ->
  regset_inject j rs rs' ->
  Mem.inject j m m' ->
  (forall id, In id (globals_of_builtin_arg a) -> kept id) ->
  exists v',
     eval_builtin_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' a v'
  /\ Val.inject j v v'.

Lemma eval_builtin_args_inject:
  forall rs sp m j rs' sp' m' al vl,
  eval_builtin_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl ->
  j sp = Some(sp', 0) ->
  meminj_preserves_globals j ->
  regset_inject j rs rs' ->
  Mem.inject j m m' ->
  (forall id, In id (globals_of_builtin_args al) -> kept id) ->
  exists vl',
     eval_builtin_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' al vl'
  /\ Val.inject_list j vl vl'.

Theorem step_simulation:
  forall S1 t S2, step ge S1 t S2 ->
  forall S1' (MS: match_states S1 S1'),
  exists S2', step tge S1' t S2' /\ match_states S2 S2'.


Remark init_meminj_no_overlap:
  forall m, Mem.meminj_no_overlap init_meminj m.

Lemma store_zeros_unmapped_inj:
  forall m1 b1 i n m1',
  store_zeros m1 b1 i n = Some m1' ->
  forall m2,
  Mem.mem_inj init_meminj m1 m2 ->
  init_meminj b1 = None ->
  Mem.mem_inj init_meminj m1' m2.

Lemma store_zeros_mapped_inj:
  forall m1 b1 i n m1',
  store_zeros m1 b1 i n = Some m1' ->
  forall m2 b2,
  Mem.mem_inj init_meminj m1 m2 ->
  init_meminj b1 = Some(b2, 0) ->
  exists m2', store_zeros m2 b2 i n = Some m2' /\ Mem.mem_inj init_meminj m1' m2'.

Lemma store_init_data_unmapped_inj:
  forall m1 b1 i id m1' m2,
  Genv.store_init_data ge m1 b1 i id = Some m1' ->
  Mem.mem_inj init_meminj m1 m2 ->
  init_meminj b1 = None ->
  Mem.mem_inj init_meminj m1' m2.

Lemma store_init_data_mapped_inj:
  forall m1 b1 i init m1' b2 m2,
  Genv.store_init_data ge m1 b1 i init = Some m1' ->
  Mem.mem_inj init_meminj m1 m2 ->
  init_meminj b1 = Some(b2, 0) ->
  (forall id ofs, init = Init_addrof id ofs -> kept id) ->
  exists m2', Genv.store_init_data tge m2 b2 i init = Some m2' /\ Mem.mem_inj init_meminj m1' m2'.

 Lemma store_init_data_list_unmapped_inj:
  forall initlist m1 b1 i m1' m2,
  Genv.store_init_data_list ge m1 b1 i initlist = Some m1' ->
  Mem.mem_inj init_meminj m1 m2 ->
  init_meminj b1 = None ->
  Mem.mem_inj init_meminj m1' m2.

Lemma store_init_data_list_mapped_inj:
  forall initlist m1 b1 i m1' b2 m2,
  Genv.store_init_data_list ge m1 b1 i initlist = Some m1' ->
  Mem.mem_inj init_meminj m1 m2 ->
  init_meminj b1 = Some(b2, 0) ->
  (forall id ofs, In (Init_addrof id ofs) initlist -> kept id) ->
  exists m2', Genv.store_init_data_list tge m2 b2 i initlist = Some m2' /\ Mem.mem_inj init_meminj m1' m2'.

Lemma alloc_global_unmapped_inj:
  forall m1 id g m1' m2,
  Genv.alloc_global ge m1 (id, g) = Some m1' ->
  Mem.mem_inj init_meminj m1 m2 ->
  init_meminj (Mem.nextblock m1) = None ->
  Mem.mem_inj init_meminj m1' m2.

Lemma alloc_global_mapped_inj:
  forall m1 id g m1' m2,
  Genv.alloc_global ge m1 (id, g) = Some m1' ->
  Mem.mem_inj init_meminj m1 m2 ->
  init_meminj (Mem.nextblock m1) = Some(Mem.nextblock m2, 0) ->
  (forall id, ref_def g id -> kept id) ->
  exists m2',
    Genv.alloc_global tge m2 (id, g) = Some m2' /\ Mem.mem_inj init_meminj m1' m2'.

Lemma alloc_globals_app:
  forall F V (g: Genv.t F V) defs1 m defs2,
  Genv.alloc_globals g m (defs1 ++ defs2) =
  match Genv.alloc_globals g m defs1 with
  | None => None
  | Some m1 => Genv.alloc_globals g m1 defs2
  end.

Lemma alloc_globals_snoc:
  forall F V (g: Genv.t F V) m defs1 id_def,
  Genv.alloc_globals g m (defs1 ++ id_def :: nil) =
  match Genv.alloc_globals g m defs1 with
  | None => None
  | Some m1 => Genv.alloc_global g m1 id_def
  end.

Lemma alloc_globals_inj:
  forall pubs defs m1 u g1 g2,
  Genv.alloc_globals ge Mem.empty (List.rev defs) = Some m1 ->
  g1 = Genv.add_globals (Genv.empty_genv _ _ pubs) (List.rev defs) ->
  g2 = Genv.add_globals (Genv.empty_genv _ _ pubs) (filter_globdefs u nil defs) ->
  Mem.nextblock m1 = Genv.genv_next g1 ->
  (forall id, IS.In id u -> Genv.find_symbol g1 id = Genv.find_symbol ge id) ->
  (forall id, IS.In id u -> Genv.find_symbol g2 id = Genv.find_symbol tge id) ->
  (forall b id, Genv.find_symbol ge id = Some b -> Plt b (Mem.nextblock m1) -> kept id -> IS.In id u) ->
  (forall id, IS.In id u -> (fold_left add_def_prog_map (List.rev defs) (PTree.empty _))!id = pm!id) ->
  exists m2,
     Genv.alloc_globals tge Mem.empty (filter_globdefs u nil defs) = Some m2
  /\ Mem.nextblock m2 = Genv.genv_next g2
  /\ Mem.mem_inj init_meminj m1 m2.

Theorem init_mem_inject:
  forall m,
  Genv.init_mem p = Some m ->
  exists f tm, Genv.init_mem tp = Some tm /\ Mem.inject f m tm /\ meminj_preserves_globals f.

Lemma transf_initial_states:
  forall S1, initial_state p S1 -> exists S2, initial_state tp S2 /\ match_states S1 S2.

Lemma transf_final_states:
  forall S1 S2 r,
  match_states S1 S2 -> final_state S1 r -> final_state S2 r.

Theorem transf_program_correct:
  forward_simulation (semantics p) (semantics tp).

End SOUNDNESS.