Library Reloadtyping

Proof of type preservation for Reload and of correctness of computation of stack bounds for Linear.





Require Import Coqlib.

Require Import Maps.

Require Import AST.

Require Import Op.

Require Import Locations.

Require Import LTLin.

Require Import LTLintyping.

Require Import Linear.

Require Import Lineartyping.

Require Import Conventions.

Require Import Parallelmove.

Require Import Reload.

Require Import Reloadproof.

Typing Linear constructors

We show that the Linear constructor functions defined in Reload generate well-typed instruction sequences, given sufficient typing and well-formedness hypotheses over the locations involved.





Hint Resolve wt_Lgetstack wt_Lsetstack wt_Lopmove

             wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall

             wt_Llabel wt_Lgoto wt_Lcond wt_Ljumptable wt_Lreturn: reloadty.




Remark wt_code_cons:

  forall f i c, wt_instr f i -> wt_code f c -> wt_code f (i :: c).






Hint Resolve wt_code_cons: reloadty.




Definition loc_valid (f: function) (l: loc) :=

  match l with R _ => True | S s => slot_valid f s end.




Lemma loc_acceptable_valid:

  forall f l, loc_acceptable l -> loc_valid f l.






Definition loc_writable (l: loc) :=

  match l with R _ => True | S s => slot_writable s end.




Lemma loc_acceptable_writable:

  forall l, loc_acceptable l -> loc_writable l.






Hint Resolve loc_acceptable_valid loc_acceptable_writable: reloadty.




Definition locs_valid (f: function) (ll: list loc) :=

  forall l, In l ll -> loc_valid f l.

Definition locs_writable (ll: list loc) :=

  forall l, In l ll -> loc_writable l.




Lemma locs_acceptable_valid:

  forall f ll, locs_acceptable ll -> locs_valid f ll.






Lemma locs_acceptable_writable:

  forall ll, locs_acceptable ll -> locs_writable ll.






Hint Resolve locs_acceptable_valid locs_acceptable_writable: reloadty.




Lemma wt_add_reload:

  forall f src dst k,

  loc_valid f src -> Loc.type src = mreg_type dst ->

  wt_code f k -> wt_code f (add_reload src dst k).






Hint Resolve wt_add_reload: reloadty.




Lemma wt_add_reloads:

  forall f srcs dsts k,

  locs_valid f srcs -> map Loc.type srcs = map mreg_type dsts ->

  wt_code f k -> wt_code f (add_reloads srcs dsts k).






Hint Resolve wt_add_reloads: reloadty.




Lemma wt_add_spill:

  forall f src dst k,

  loc_valid f dst -> loc_writable dst -> Loc.type dst = mreg_type src ->

  wt_code f k -> wt_code f (add_spill src dst k).






Hint Resolve wt_add_spill: reloadty.




Lemma wt_add_move:

  forall f src dst k,

  loc_valid f src -> loc_valid f dst -> loc_writable dst ->

  Loc.type dst = Loc.type src ->

  wt_code f k -> wt_code f (add_move src dst k).






Hint Resolve wt_add_move: reloadty.




Lemma wt_add_moves:

  forall f b moves,

  (forall s d, In (s, d) moves ->

      loc_valid f s /\ loc_valid f d /\ loc_writable d /\ Loc.type s = Loc.type d) ->

  wt_code f b ->

  wt_code f 

    (List.fold_right (fun p k => add_move (fst p) (snd p) k) b moves).






Theorem wt_parallel_move:

 forall f srcs dsts b,

 List.map Loc.type srcs = List.map Loc.type dsts ->

 locs_valid f srcs -> locs_valid f dsts -> locs_writable dsts ->

 wt_code f b ->  wt_code f (parallel_move srcs dsts b).



Hint Resolve wt_parallel_move: reloadty.




Lemma wt_reg_for:

  forall l, mreg_type (reg_for l) = Loc.type l.



Hint Resolve wt_reg_for: reloadty.




Lemma wt_regs_for_rec:

  forall locs itmps ftmps,

  enough_temporaries_rec locs itmps ftmps = true ->

  (forall r, In r itmps -> mreg_type r = Tint) ->

  (forall r, In r ftmps -> mreg_type r = Tfloat) ->

  List.map mreg_type (regs_for_rec locs itmps ftmps) = List.map Loc.type locs.






Lemma wt_regs_for:

  forall locs,

  enough_temporaries locs = true ->

  List.map mreg_type (regs_for locs) = List.map Loc.type locs.



Hint Resolve wt_regs_for: reloadty.




Hint Resolve enough_temporaries_op_args enough_temporaries_cond enough_temporaries_addr: reloadty.




Hint Extern 4 (_ = _) => congruence : reloadty.




Lemma wt_transf_instr:

  forall f instr k,

  LTLintyping.wt_instr (LTLin.fn_sig f) instr ->

  wt_code (transf_function f) k ->

  wt_code (transf_function f) (transf_instr f instr k).






Lemma wt_transf_code:

  forall f  c,

  LTLintyping.wt_code (LTLin.fn_sig f) c ->

  Lineartyping.wt_code (transf_function f) (transf_code f c).






Lemma wt_transf_fundef:

  forall fd,

  LTLintyping.wt_fundef fd ->

  Lineartyping.wt_fundef (transf_fundef fd).






Lemma program_typing_preserved:

  forall p,

  LTLintyping.wt_program p ->

  Lineartyping.wt_program (transf_program p).