Module Lineartyping

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Globalenvs.
Require Import Memory.
Require Import Events.
Require Import Op.
Require Import Machregs.
Require Import Locations.
Require Import Conventions.
Require Import LTL.
Require Import Linear.

Require Import Values_symbolic.
Require Import Values_symbolictype.




Lemma eval_addressing_wt:
  forall F V (ge: Genv.t F V) sp a args v
         (EOP : eval_addressing ge sp a args = Some v),
    weak_wt v Tint.

Lemma eval_condition_wt:
  forall c l v
         (EOP : eval_condition c l = Some v),
    weak_wt v Tint.

Lemma eval_operation_wt:
  forall F V (ge : Genv.t F V) sp op args v
         (EOP : eval_operation ge sp op args = Some v)
         (diff: op <> Omove),
    weak_wt v (Normalise.styp_of_typ (snd (type_of_operation op))).


Section WT_INSTR.

Variable funct: function.

Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool :=
  match sl with
  | Local => zle 0 ofs
  | Outgoing => zle 0 ofs
  | Incoming => In_dec Loc.eq (S Incoming ofs ty) (loc_parameters funct.(fn_sig))
  end &&
  match ty with AST.Tlong => false | _ => true end.

Definition slot_writable (sl: slot) : bool :=
  match sl with
  | Local => true
  | Outgoing => true
  | Incoming => false
  end.

Definition loc_valid (l: loc) : bool :=
  match l with
  | R r => true
  | S Local ofs ty => slot_valid Local ofs ty
  | S _ _ _ => false
  end.


Fixpoint reg_has_typ_list (ml: list mreg) (tl: list typ) : bool :=
  match ml, tl with
      nil, nil => true
    | r::ml,t::tl => subtype (mreg_type r) t && reg_has_typ_list ml tl
    | _, _ => false
  end.

Fixpoint subtype_list (lt1 lt2: list typ) : bool :=
  match lt1, lt2 with
      nil, nil => true
    | t1::lt1, t2:: lt2 => subtype t1 t2 && subtype_list lt1 lt2
    | _, _ => false
  end.

Definition wt_instr (i: instruction) : bool :=
  match i with
  | Lgetstack sl ofs ty r =>
      subtype ty (mreg_type r) && slot_valid sl ofs ty
  | Lsetstack r sl ofs ty =>
    subtype ty (mreg_type r) &&
            slot_valid sl ofs ty && slot_writable sl
  | Lop op args res =>
      match is_move_operation op args with
      | Some arg =>
          subtype (mreg_type arg) (mreg_type res)
      | None =>
          let (targs, tres) := type_of_operation op in
          subtype tres (mreg_type res)
      end
  | Lload chunk addr args dst =>
      subtype (AST.type_of_chunk chunk) (mreg_type dst)
  | Ltailcall sg ros =>
      zeq (size_arguments sg) 0
  | Lbuiltin ef args res =>
      subtype_list (proj_sig_res' (ef_sig ef)) (map mreg_type res)
  | _ =>
      true
  end.

End WT_INSTR.

Definition wt_code (f: function) (c: code) : bool :=
  forallb (wt_instr f) c.

Definition wt_function (f: function) : bool :=
  wt_code f f.(fn_code).


Definition wt_locset (ls: locset) : Prop :=
  forall l, wt (ls l) (Loc.type l).

Lemma locmap_set_reg_rew:
  forall l v ls p,
    Locmap.set (R l) v ls p =
    if Loc.eq (R l) p then v else ls p.

Lemma wt_setreg:
  forall ls r v,
    wt v (mreg_type r) -> wt_locset ls -> wt_locset (Locmap.set (R r) v ls).

Lemma wt_setstack:
  forall ls sl ofs ty v,
    wt_locset ls -> wt_locset (Locmap.set (S sl ofs ty) v ls).

Lemma wt_undef_regs:
  forall rs ls, wt_locset ls -> wt_locset (undef_regs rs ls).

Lemma wt_call_regs:
  forall ls, wt_locset ls -> wt_locset (call_regs ls).

Lemma wt_return_regs:
  forall caller callee,
  wt_locset caller -> wt_locset callee -> wt_locset (return_regs caller callee).

Lemma wt_init:
  wt_locset (Locmap.init ).

Lemma wt_setlist:
  forall vl rl rs,
    list_forall2 wt vl (map mreg_type rl) ->
    wt_locset rs ->
    wt_locset (Locmap.setlist (map R rl) vl rs).

Lemma wt_find_label:
  forall f lbl c,
  wt_function f = true ->
  find_label lbl f.(fn_code) = Some c ->
  wt_code f c = true.


Definition wt_fundef (fd: fundef) :=
  match fd with
  | Internal f => wt_function f = true
  | External ef => True
  end.


Definition wt_sp (sp: expr_sym) : Prop :=
  Val.has_type sp Tint.


Inductive wt_callstack: list stackframe -> Prop :=
  | wt_callstack_nil:
      wt_callstack nil
  | wt_callstack_cons: forall f sp rs c s
        (WTSTK: wt_callstack s)
        (WTF: wt_function f = true)
        (WTC: wt_code f c = true)
        (WTRS: wt_locset rs)
        (WTSP: wt_sp sp),
      wt_callstack (Stackframe f sp rs c :: s).

Lemma wt_parent_locset:
  forall s, wt_callstack s -> wt_locset (parent_locset s).

Inductive wt_state: state -> Prop :=
  | wt_regular_state: forall s f sp c rs m
        (WTSTK: wt_callstack s )
        (WTF: wt_function f = true)
        (WTC: wt_code f c = true)
        (WTRS: wt_locset rs)
        (WTSP: wt_sp sp),
      wt_state (State s f sp c rs m)
  | wt_call_state: forall s fd rs m
        (WTSTK: wt_callstack s)
        (WTFD: wt_fundef fd)
        (WTRS: wt_locset rs),
      wt_state (Callstate s fd rs m)
  | wt_return_state: forall s rs m
        (WTSTK: wt_callstack s)
        (WTRS: wt_locset rs),
      wt_state (Returnstate s rs m).


Section SOUNDNESS.

Variable prog: program.
Let ge := Genv.globalenv prog.

Hypothesis wt_prog:
  forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd.

Lemma wt_find_function:
  forall m ros rs f, find_function ge m ros rs = Some f -> wt_fundef f.


Lemma reg_type_list_args_type_list:
  forall rs args ty_args args'
         (WTRS : wt_locset rs)
         (RS: (reglist rs args) = args')
         (H4 : reg_has_typ_list args ty_args = true),
    list_forall2 wt args' ty_args.

Lemma wt_trans:
  forall a t1 t2,
    subtype t1 t2 = true ->
    wt a t1 ->
    wt a t2.

Lemma subtype_list_has_type_list:
  forall (l l0 : list typ) (vl : list expr_sym),
    subtype_list l0 l = true ->
    list_forall2 wt vl ( l0) ->
    list_forall2 wt vl ( l).

Lemma list_forall2_map:
  forall { X Y Y' } (P: X -> Y' -> Prop) (f: Y -> Y') l l'
    (LF2: list_forall2 P l (map f l')),
    list_forall2 (fun x y => P x (f y)) l l'.
  
Theorem step_type_preservation:
  forall ns S1 t S2, step ge ns S1 t S2 -> wt_state S1 -> wt_state S2.

Theorem wt_initial_state:
  forall sg S, initial_state prog sg S -> wt_state S.

End SOUNDNESS.


Lemma wt_state_getstack:
  forall s f sp sl ofs ty rd c rs m,
  wt_state (State s f sp (Lgetstack sl ofs ty rd :: c) rs m) ->
  slot_valid f sl ofs ty = true.

Lemma wt_state_setstack:
  forall s f sp sl ofs ty r c rs m,
  wt_state (State s f sp (Lsetstack r sl ofs ty :: c) rs m) ->
  slot_valid f sl ofs ty = true /\ slot_writable sl = true.

Lemma wt_state_tailcall:
  forall s f sp sg ros c rs m,
  wt_state (State s f sp (Ltailcall sg ros :: c) rs m) ->
  size_arguments sg = 0.


Lemma wt_callstate_wt_regs:
  forall s f rs m,
  wt_state (Callstate s f rs m) ->
  forall r, wt (rs (R r)) (mreg_type r).