(** Typing rules and a type inference algorithm for RTL. *)

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Conventions.

(** * The type system *)

(** Like Cminor and all intermediate languages, RTL can be equipped with
  a simple type system that statically guarantees that operations
  and addressing modes are applied to the right number of arguments
  and that the arguments are of the correct types.  The type algebra
  is trivial, consisting of the two types [Tint] (for integers and pointers)
  and [Tfloat] (for floats).  

  Additionally, we impose that each pseudo-register has the same type
  throughout the function.  This requirement helps with register allocation,
  enabling each pseudo-register to be mapped to a single hardware register
  or stack location of the correct type.


  The typing judgement for instructions is of the form [wt_instr f env instr],
  where [f] is the current function (used to type-check [Ireturn] 
  instructions) and [env] is a typing environment associating types to
  pseudo-registers.  Since pseudo-registers have unique types throughout
  the function, the typing environment does not change during type-checking
  of individual instructions.  One point to note is that we have two
  polymorphic operators, [Omove] and [Oundef], which can work both
  over integers and floats.
*)

Definition regenv := reg -> typ.

Section WT_INSTR.

Variable env: regenv.
Variable funsig: signature.

Inductive wt_instr : instruction -> Prop :=
  | wt_Inop:
      forall s,
      wt_instr (Inop s)
  | wt_Iopmove:
      forall r1 r s,
      env r1 = env r ->
      wt_instr (Iop Omove (r1 :: nil) r s)
  | wt_Iopundef:
      forall r s,
      wt_instr (Iop Oundef nil r s)
  | wt_Iop:
      forall op args res s,
      op <> Omove -> op <> Oundef ->
      (List.map env args, env res) = type_of_operation op ->
      wt_instr (Iop op args res s)
  | wt_Iload:
      forall chunk addr args dst s,
      List.map env args = type_of_addressing addr ->
      env dst = type_of_chunk chunk ->
      wt_instr (Iload chunk addr args dst s)
  | wt_Istore:
      forall chunk addr args src s,
      List.map env args = type_of_addressing addr ->
      env src = type_of_chunk chunk ->
      wt_instr (Istore chunk addr args src s)
  | wt_Icall:
      forall sig ros args res s,
      match ros with inl r => env r = Tint | inr s => True end ->
      List.map env args = sig.(sig_args) ->
      env res = match sig.(sig_res) with None => Tint | Some ty => ty end ->
      wt_instr (Icall sig ros args res s)
  | wt_Ialloc:
      forall arg res s,
      env arg = Tint -> env res = Tint ->
      wt_instr (Ialloc arg res s)
  | wt_Icond:
      forall cond args s1 s2,
      List.map env args = type_of_condition cond ->
      wt_instr (Icond cond args s1 s2)
  | wt_Ireturn: 
      forall optres,
      option_map env optres = funsig.(sig_res) ->
      wt_instr (Ireturn optres).

End WT_INSTR.

(** A function [f] is well-typed w.r.t. a typing environment [env],
   written [wt_function env f], if all instructions are well-typed,
   parameters agree in types with the function signature, and
   names of parameters are pairwise distinct. *)

Record wt_function (f: function) (env: regenv): Prop :=
  mk_wt_function {
    wt_params:
      List.map env f.(fn_params) = f.(fn_sig).(sig_args);
    wt_norepet:
      list_norepet f.(fn_params);
    wt_instrs:
      forall pc instr, 
      f.(fn_code)!pc = Some instr -> wt_instr env f.(fn_sig) instr
}.

Inductive wt_fundef: fundef -> Prop :=
  | wt_fundef_external: forall ef,
      Conventions.sig_external_ok ef.(ef_sig) ->
      wt_fundef (External ef)
  | wt_function_internal: forall f env,
      wt_function f env ->
      wt_fundef (Internal f).

Definition wt_program (p: program): Prop :=
  forall i f, In (i, f) (prog_funct p) -> wt_fundef f.

(** * Type inference *)

(** There are several ways to ensure that RTL code is well-typed and
  to obtain the typing environment (type assignment for pseudo-registers)
  needed for register allocation.  One is to start with well-typed Cminor
  code and show type preservation for RTL generation and RTL optimizations.
  Another is to start with untyped RTL and run a type inference algorithm
  that reconstructs the typing environment, determining the type of
  each pseudo-register from its uses in the code.  We follow the second
  approach.

  We delegate the task of determining the type of each pseudo-register
  to an external ``oracle'': a function written in Caml and not
  proved correct.  We verify the returned type environment using
  the following Coq code, which we will prove correct. *)

Parameter infer_type_environment:
  function -> list (node * instruction) -> option regenv.

(** ** Algorithm to check the correctness of a type environment *)

Section TYPECHECKING.

Variable funct: function.
Variable env: regenv.

Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}.
Proof. decide equality. Qed.

Definition check_reg (r: reg) (ty: typ): bool :=
  if typ_eq (env r) ty then true else false.

Fixpoint check_regs (rl: list reg) (tyl: list typ) {struct rl}: bool :=
  match rl, tyl with
  | nil, nil => true
  | r1::rs, ty::tys => check_reg r1 ty && check_regs rs tys
  | _, _ => false
  end.

Definition check_op (op: operation) (args: list reg) (res: reg): bool :=
  let (targs, tres) := type_of_operation op in
  check_regs args targs && check_reg res tres.

Definition check_instr (i: instruction) : bool :=
  match i with
  | Inop _ =>
      true
  | Iop Omove (arg::nil) res _ =>
      if typ_eq (env arg) (env res) then true else false
  | Iop Omove args res _ =>
      false
  | Iop Oundef nil res _ =>
      true
  | Iop Oundef args res _ =>
      false
  | Iop op args res _ =>
      check_op op args res
  | Iload chunk addr args dst _ =>
      check_regs args (type_of_addressing addr)
      && check_reg dst (type_of_chunk chunk)
  | Istore chunk addr args src _ =>
      check_regs args (type_of_addressing addr)
      && check_reg src (type_of_chunk chunk)
  | Icall sig ros args res _ =>
      match ros with inl r => check_reg r Tint | inr s => true end
      && check_regs args sig.(sig_args)
      && check_reg res (match sig.(sig_res) with None => Tint | Some ty => ty end)
  | Ialloc arg res _ =>
      check_reg arg Tint && check_reg res Tint
  | Icond cond args _ _ =>
      check_regs args (type_of_condition cond)
  | Ireturn optres =>
      match optres, funct.(fn_sig).(sig_res) with
      | None, None => true
      | Some r, Some t => check_reg r t
      | _, _ => false
      end
  end.

Definition check_params_norepet (params: list reg): bool :=
  if list_norepet_dec Reg.eq params then true else false.

Fixpoint check_instrs (instrs: list (node * instruction)) : bool :=
  match instrs with
  | nil => true
  | (pc, i) :: rem => check_instr i && check_instrs rem
  end.

(** ** Correctness of the type-checking algorithm *)

Lemma check_reg_correct:
  forall r ty, check_reg r ty = true -> env r = ty.
Proof.
  unfold check_reg; intros.
  destruct (typ_eq (env r) ty). auto. discriminate.
Qed.

Lemma check_regs_correct:
  forall rl tyl, check_regs rl tyl = true -> List.map env rl = tyl.
Proof.
  induction rl; destruct tyl; simpl; intros.
  auto. discriminate. discriminate.
  elim (andb_prop _ _ H); intros. 
  rewrite (check_reg_correct _ _ H0). rewrite (IHrl tyl H1). auto.
Qed.

Lemma check_op_correct:
  forall op args res,
  check_op op args res = true ->
  (List.map env args, env res) = type_of_operation op.
Proof.
  unfold check_op; intros.
  destruct (type_of_operation op) as [targs tres]. 
  elim (andb_prop _ _ H); intros.
  rewrite (check_regs_correct _ _ H0).
  rewrite (check_reg_correct _ _ H1).
  auto.
Qed.

Lemma check_instr_correct:
  forall i, check_instr i = true -> wt_instr env funct.(fn_sig) i.
Proof.
  unfold check_instr; intros; destruct i.
  (* nop *)
  constructor.
  (* op *)
  destruct o;
  try (apply wt_Iop; [congruence|congruence|apply check_op_correct;auto]).
  destruct l; try discriminate. destruct l; try discriminate.
  destruct (typ_eq (env r0) (env r)); try discriminate.
  apply wt_Iopmove; auto.
  destruct l; try discriminate.
  apply wt_Iopundef.
  (* load *)
  elim (andb_prop _ _ H); intros.
  constructor. apply check_regs_correct; auto. apply check_reg_correct; auto.
  (* store *)
  elim (andb_prop _ _ H); intros.
  constructor. apply check_regs_correct; auto. apply check_reg_correct; auto.
  (* call *)
  elim (andb_prop _ _ H); clear H; intros.
  elim (andb_prop _ _ H); clear H; intros.
  constructor.
  destruct s0; auto. apply check_reg_correct; auto.
  apply check_regs_correct; auto.
  apply check_reg_correct; auto.
  (* alloc *)
  elim (andb_prop _ _ H); intros.
  constructor; apply check_reg_correct; auto.
  (* cond *)
  constructor. apply check_regs_correct; auto.
  (* return *)
  constructor. 
  destruct o; simpl; destruct funct.(fn_sig).(sig_res); try discriminate.
  rewrite (check_reg_correct _ _ H); auto.
  auto.
Qed.

Lemma check_instrs_correct:
  forall instrs,
  check_instrs instrs = true ->
  forall pc i, In (pc, i) instrs -> wt_instr env funct.(fn_sig) i.
Proof.
  induction instrs; simpl; intros.
  elim H0.
  destruct a as [pc' i']. elim (andb_prop _ _ H); clear H; intros.
  elim H0; intro.
  inversion H2; subst pc' i'. apply check_instr_correct; auto.
  eauto.
Qed.

End TYPECHECKING.

(** ** The type inference function **)

Definition type_function (f: function): option regenv :=
  let instrs := PTree.elements f.(fn_code) in
  match infer_type_environment f instrs with
  | None => None
  | Some env =>
      if check_regs env f.(fn_params) f.(fn_sig).(sig_args)
      && check_params_norepet f.(fn_params)
      && check_instrs f env instrs
      then Some env else None
  end.

Definition type_external_function (ef: external_function): bool :=
  List.fold_right
    (fun l b => match l with Locations.S _ => false | Locations.R _ => b end)
    true (Conventions.loc_arguments ef.(ef_sig)).

Lemma type_function_correct:
  forall f env,
  type_function f = Some env ->
  wt_function f env.
Proof.
  unfold type_function; intros until env.
  set (instrs := PTree.elements f.(fn_code)).
  case (infer_type_environment f instrs).
  intro env'. 
  caseEq (check_regs env' f.(fn_params) f.(fn_sig).(sig_args)); intro; simpl; try congruence.
  caseEq (check_params_norepet f.(fn_params)); intro; simpl; try congruence.
  caseEq (check_instrs f env' instrs); intro; simpl; try congruence.
  intro EQ; inversion EQ; subst env'.
  constructor. 
  apply check_regs_correct; auto.
  unfold check_params_norepet in H0. 
  destruct (list_norepet_dec Reg.eq (fn_params f)). auto. discriminate.
  intros. eapply check_instrs_correct. eauto. 
  unfold instrs. apply PTree.elements_correct. eauto.
  congruence.
Qed.

Lemma type_external_function_correct:
  forall ef,
  type_external_function ef = true ->
  Conventions.sig_external_ok ef.(ef_sig).
Proof.
  intro ef. unfold type_external_function, Conventions.sig_external_ok.
  generalize (Conventions.loc_arguments (ef_sig ef)).
  induction l; simpl.
  tauto.
  destruct a. intros. firstorder congruence.
  congruence.
Qed.

(** * Type preservation during evaluation *)

(** The type system for RTL is not sound in that it does not guarantee
  progress: well-typed instructions such as [Icall] can fail because
  of run-time type tests (such as the equality between calle and caller's
  signatures).  However, the type system guarantees a type preservation
  property: if the execution does not fail because of a failed run-time
  test, the result values and register states match the static
  typing assumptions.  This preservation property will be useful
  later for the proof of semantic equivalence between [Machabstr] and [Mach].
  Even though we do not need it for [RTL], we show preservation for [RTL]
  here, as a warm-up exercise and because some of the lemmas will be
  useful later. *)

Require Import Globalenvs.
Require Import Values.
Require Import Mem.
Require Import Integers.
Require Import Events.

Definition wt_regset (env: regenv) (rs: regset) : Prop :=
  forall r, Val.has_type (rs#r) (env r).

Lemma wt_regset_assign:
  forall env rs v r,
  wt_regset env rs ->
  Val.has_type v (env r) ->
  wt_regset env (rs#r <- v).
Proof.
  intros; red; intros. 
  rewrite Regmap.gsspec.
  case (peq r0 r); intro.
  subst r0. assumption.
  apply H.
Qed.

Lemma wt_regset_list:
  forall env rs,
  wt_regset env rs ->
  forall rl, Val.has_type_list (rs##rl) (List.map env rl).
Proof.
  induction rl; simpl.
  auto.
  split. apply H. apply IHrl.
Qed.  

Lemma wt_init_regs:
  forall env rl args,
  Val.has_type_list args (List.map env rl) ->
  wt_regset env (init_regs args rl).
Proof.
  induction rl; destruct args; simpl; intuition.
  red; intros. rewrite Regmap.gi. simpl; auto. 
  apply wt_regset_assign; auto.
Qed.

Lemma wt_event_match:
  forall ef args t res,
  event_match ef args t res ->
  Val.has_type res (proj_sig_res ef.(ef_sig)).
Proof.
  induction 1. inversion H0; exact I.
Qed.

Section SUBJECT_REDUCTION.

Variable p: program.

Hypothesis wt_p: wt_program p.

Let ge := Genv.globalenv p.

Definition exec_instr_subject_reduction
    (c: code) (sp: val)
    (pc: node) (rs: regset) (m: mem) (t: trace)
    (pc': node) (rs': regset) (m': mem) : Prop :=
  forall env f
         (CODE: c = fn_code f)
         (WT_FN: wt_function f env)
         (WT_RS: wt_regset env rs),
  wt_regset env rs'.

Definition exec_function_subject_reduction
    (f: fundef) (args: list val) (m: mem) (t: trace) (res: val) (m': mem) : Prop :=
  wt_fundef f ->  
  Val.has_type_list args (sig_args (funsig f)) ->
  Val.has_type res (proj_sig_res (funsig f)).

Lemma subject_reduction:
  forall f args m t res m',
  exec_function ge f args m t res m' ->
  exec_function_subject_reduction f args m t res m'.
Proof.
  apply (exec_function_ind_3 ge
           exec_instr_subject_reduction
           exec_instr_subject_reduction
           exec_function_subject_reduction);
  intros; red; intros;
  try (rewrite CODE in H;
       generalize (wt_instrs _ _ WT_FN pc _ H);
       intro WT_INSTR;
       inversion WT_INSTR).
 
  assumption.

  apply wt_regset_assign. auto. 
  subst op. subst args. simpl in H0. injection H0; intro. 
  subst v. rewrite <- H2. apply WT_RS.

  apply wt_regset_assign. auto.
  subst op; subst args; simpl in H0. injection H0; intro; subst v.
  simpl; auto.

  apply wt_regset_assign. auto.
  replace (env res) with (snd (type_of_operation op)).
  apply type_of_operation_sound with fundef ge rs##args sp; auto.
  rewrite <- H7. reflexivity.

  apply wt_regset_assign. auto. rewrite H8. 
  eapply type_of_chunk_correct; eauto.

  assumption.

  apply wt_regset_assign. auto. rewrite H11. rewrite <- H1.
  assert (wt_fundef f).
    destruct ros; simpl in H0.
    pattern f. apply Genv.find_funct_prop with fundef p (rs#r).
    exact wt_p. exact H0. 
    caseEq (Genv.find_symbol ge i); intros; rewrite H12 in H0.
    pattern f. apply Genv.find_funct_ptr_prop with fundef p b.
    exact wt_p. exact H0.
    discriminate.
  eapply H3. auto. rewrite H1. rewrite <- H10.
  apply wt_regset_list; auto. 

  apply wt_regset_assign. auto. rewrite H6; exact I. 

  assumption.
  assumption.
  assumption.
  eauto.
  eauto.

  inversion H4; subst f0.
  assert (WT_INIT: wt_regset env (init_regs args (fn_params f))).
    apply wt_init_regs. rewrite (wt_params _ _ H7). assumption.
  generalize (H1 env f (refl_equal (fn_code f)) H7 WT_INIT). 
  intro WT_RS.
  generalize (wt_instrs _ _ H7 pc _ H2).
  intro WT_INSTR; inversion WT_INSTR.
  unfold proj_sig_res; simpl.
  destruct or; simpl in H3; simpl in H8; rewrite <- H8.
  rewrite H3. apply WT_RS. 
  rewrite H3. simpl; auto.

  simpl. eapply wt_event_match; eauto.
Qed. 

End SUBJECT_REDUCTION.