Require Import Coqlib Maps Errors.
Require Import AST Integers Floats Values Memory Globalenvs Events Smallstep.
Require Import Cminor.
Require Import Unityping.

Local Open Scope string_scope.
Local Open Scope error_monad_scope.

Type inference algorithm

Definition type_constant (c: constant) : typ :=
  match c with
  | Ointconst _ => Tint
  | Ofloatconst _ => Tfloat
  | Osingleconst _ => Tsingle
  | Olongconst _ => Tlong
  | Oaddrsymbol _ _ => Tptr
  | Oaddrstack _ => Tptr
  end.

Definition type_unop (op: unary_operation) : typ * typ :=
  match op with
  | Ocast8unsigned | Ocast8signed | Ocast16unsigned | Ocast16signed
  | Onegint | Onotint => (Tint, Tint)
  | Onegf | Oabsf => (Tfloat, Tfloat)
  | Onegfs | Oabsfs => (Tsingle, Tsingle)
  | Osingleoffloat => (Tfloat, Tsingle)
  | Ofloatofsingle => (Tsingle, Tfloat)
  | Ointoffloat | Ointuoffloat => (Tfloat, Tint)
  | Ofloatofint | Ofloatofintu => (Tint, Tfloat)
  | Ointofsingle | Ointuofsingle => (Tsingle, Tint)
  | Osingleofint | Osingleofintu => (Tint, Tsingle)
  | Onegl | Onotl => (Tlong, Tlong)
  | Ointoflong => (Tlong, Tint)
  | Olongofint | Olongofintu => (Tint, Tlong)
  | Olongoffloat | Olonguoffloat => (Tfloat, Tlong)
  | Ofloatoflong | Ofloatoflongu => (Tlong, Tfloat)
  | Olongofsingle | Olonguofsingle => (Tsingle, Tlong)
  | Osingleoflong | Osingleoflongu => (Tlong, Tsingle)
  end.

Definition type_binop (op: binary_operation) : typ * typ * typ :=
  match op with
  | Oadd | Osub | Omul | Odiv | Odivu | Omod | Omodu
  | Oand | Oor | Oxor | Oshl | Oshr | Oshru => (Tint, Tint, Tint)
  | Oaddf | Osubf | Omulf | Odivf => (Tfloat, Tfloat, Tfloat)
  | Oaddfs| Osubfs| Omulfs| Odivfs => (Tsingle, Tsingle, Tsingle)
  | Oaddl | Osubl | Omull | Odivl | Odivlu | Omodl | Omodlu
  | Oandl | Oorl | Oxorl => (Tlong, Tlong, Tlong)
  | Oshll | Oshrl | Oshrlu => (Tlong, Tint, Tlong)
  | Ocmp _ | Ocmpu _ => (Tint, Tint, Tint)
  | Ocmpf _ => (Tfloat, Tfloat, Tint)
  | Ocmpfs _ => (Tsingle, Tsingle, Tint)
  | Ocmpl _ | Ocmplu _ => (Tlong, Tlong, Tint)
  end.

Module RTLtypes <: TYPE_ALGEBRA.

Definition t := typ.
Definition eq := typ_eq.
Definition default := Tint.

End RTLtypes.

Module S := UniSolver(RTLtypes).

Definition expect (e: S.typenv) (t1 t2: typ) : res S.typenv :=
  if typ_eq t1 t2 then OK e else Error (msg "type mismatch").

Fixpoint type_expr (e: S.typenv) (a: expr) (t: typ) : res S.typenv :=
  match a with
  | Evar id => S.set e id t
  | Econst c => expect e (type_constant c) t
  | Eunop op a1 =>
      let '(targ1, tres) := type_unop op in
      do e1 <- type_expr e a1 targ1;
      expect e1 tres t
  | Ebinop op a1 a2 =>
      let '(targ1, targ2, tres) := type_binop op in
      do e1 <- type_expr e a1 targ1;
      do e2 <- type_expr e1 a2 targ2;
      expect e2 tres t
  | Eload chunk a1 =>
      do e1 <- type_expr e a1 Tptr;
      expect e1 (type_of_chunk chunk) t
  end.

Fixpoint type_exprlist (e: S.typenv) (al: list expr) (tl: list typ) : res S.typenv :=
  match al, tl with
  | nil, nil => OK e
  | a :: al, t :: tl => do e1 <- type_expr e a t; type_exprlist e1 al tl
  | _, _ => Error (msg "arity mismatch")
  end.

Definition type_assign (e: S.typenv) (id: ident) (a: expr) : res S.typenv :=
  match a with
  | Evar id' =>
      do (changed, e1) <- S.move e id id'; OK e1
  | Econst c =>
      S.set e id (type_constant c)
  | Eunop op a1 =>
      let '(targ1, tres) := type_unop op in
      do e1 <- type_expr e a1 targ1;
      S.set e1 id tres
  | Ebinop op a1 a2 =>
      let '(targ1, targ2, tres) := type_binop op in
      do e1 <- type_expr e a1 targ1;
      do e2 <- type_expr e1 a2 targ2;
      S.set e2 id tres
  | Eload chunk a1 =>
      do e1 <- type_expr e a1 Tptr;
      S.set e1 id (type_of_chunk chunk)
  end.

Definition opt_set (e: S.typenv) (optid: option ident) (ty: typ) : res S.typenv :=
  match optid with
  | None => OK e
  | Some id => S.set e id ty
  end.

Fixpoint type_stmt (tret: rettype) (e: S.typenv) (s: stmt) : res S.typenv :=
  match s with
  | Sskip => OK e
  | Sassign id a => type_assign e id a
  | Sstore chunk a1 a2 =>
      do e1 <- type_expr e a1 Tptr; type_expr e1 a2 (type_of_chunk chunk)
  | Scall optid sg fn args =>
      do e1 <- type_expr e fn Tptr;
      do e2 <- type_exprlist e1 args sg.(sig_args);
      opt_set e2 optid (proj_sig_res sg)
  | Stailcall sg fn args =>
      assertion (rettype_eq sg.(sig_res) tret);
      do e1 <- type_expr e fn Tptr;
      type_exprlist e1 args sg.(sig_args)
  | Sbuiltin optid ef args =>
      let sg := ef_sig ef in
      do e1 <- type_exprlist e args sg.(sig_args);
      opt_set e1 optid (proj_sig_res sg)
  | Sseq s1 s2 =>
      do e1 <- type_stmt tret e s1; type_stmt tret e1 s2
  | Sifthenelse a s1 s2 =>
      do e1 <- type_expr e a Tint;
      do e2 <- type_stmt tret e1 s1;
      type_stmt tret e2 s2
  | Sloop s1 =>
      type_stmt tret e s1
  | Sblock s1 =>
      type_stmt tret e s1
  | Sexit n =>
      OK e
  | Sswitch sz a tbl dfl =>
      type_expr e a (if sz then Tlong else Tint)
  | Sreturn opta =>
      match opta with
      | None => OK e
      | Some a => type_expr e a (proj_rettype tret)
      end
  | Slabel lbl s1 =>
      type_stmt tret e s1
  | Sgoto lbl =>
      OK e
  end.

Definition typenv := ident -> typ.

Definition type_function (f: function) : res typenv :=
  do e1 <- S.set_list S.initial f.(fn_params) f.(fn_sig).(sig_args);
  do e2 <- type_stmt f.(fn_sig).(sig_res) e1 f.(fn_body);
  S.solve e2.

Relational specification of the type system

Section SPEC.

Variable env: ident -> typ.
Variable tret: rettype.

Inductive wt_expr: expr -> typ -> Prop :=
  | wt_Evar: forall id,
      wt_expr (Evar id) (env id)
  | wt_Econst: forall c,
      wt_expr (Econst c) (type_constant c)
  | wt_Eunop: forall op a1 targ1 tres,
      type_unop op = (targ1, tres) ->
      wt_expr a1 targ1 ->
      wt_expr (Eunop op a1) tres
  | wt_Ebinop: forall op a1 a2 targ1 targ2 tres,
      type_binop op = (targ1, targ2, tres) ->
      wt_expr a1 targ1 -> wt_expr a2 targ2 ->
      wt_expr (Ebinop op a1 a2) tres
  | wt_Eload: forall chunk a1,
      wt_expr a1 Tptr ->
      wt_expr (Eload chunk a1) (type_of_chunk chunk).

Definition wt_opt_assign (optid: option ident) (ty: rettype) : Prop :=
  match optid with
  | Some id => proj_rettype ty = env id
  | _ => True
  end.

Inductive wt_stmt: stmt -> Prop :=
  | wt_Sskip:
      wt_stmt Sskip
  | wt_Sassign: forall id a,
      wt_expr a (env id) ->
      wt_stmt (Sassign id a)
  | wt_Sstore: forall chunk a1 a2,
      wt_expr a1 Tptr -> wt_expr a2 (type_of_chunk chunk) ->
      wt_stmt (Sstore chunk a1 a2)
  | wt_Scall: forall optid sg a1 al,
      wt_expr a1 Tptr -> list_forall2 wt_expr al sg.(sig_args) ->
      wt_opt_assign optid sg.(sig_res) ->
      wt_stmt (Scall optid sg a1 al)
  | wt_Stailcall: forall sg a1 al,
      wt_expr a1 Tptr -> list_forall2 wt_expr al sg.(sig_args) ->
      sg.(sig_res) = tret ->
      wt_stmt (Stailcall sg a1 al)
  | wt_Sbuiltin: forall optid ef al,
      list_forall2 wt_expr al (ef_sig ef).(sig_args) ->
      wt_opt_assign optid (ef_sig ef).(sig_res) ->
      wt_stmt (Sbuiltin optid ef al)
  | wt_Sseq: forall s1 s2,
      wt_stmt s1 -> wt_stmt s2 ->
      wt_stmt (Sseq s1 s2)
  | wt_Sifthenelse: forall a s1 s2,
      wt_expr a Tint -> wt_stmt s1 -> wt_stmt s2 ->
      wt_stmt (Sifthenelse a s1 s2)
  | wt_Sloop: forall s1,
      wt_stmt s1 ->
      wt_stmt (Sloop s1)
  | wt_Sblock: forall s1,
      wt_stmt s1 ->
      wt_stmt (Sblock s1)
  | wt_Sexit: forall n,
      wt_stmt (Sexit n)
  | wt_Sswitch: forall (sz: bool) a tbl dfl,
      wt_expr a (if sz then Tlong else Tint) ->
      wt_stmt (Sswitch sz a tbl dfl)
  | wt_Sreturn_none:
      wt_stmt (Sreturn None)
  | wt_Sreturn_some: forall a,
      wt_expr a (proj_rettype tret) ->
      wt_stmt (Sreturn (Some a))
  | wt_Slabel: forall lbl s1,
      wt_stmt s1 ->
      wt_stmt (Slabel lbl s1)
  | wt_Sgoto: forall lbl,
      wt_stmt (Sgoto lbl).

End SPEC.

Inductive wt_function (env: typenv) (f: function) : Prop :=
  wt_function_intro:
    type_function f = OK env -> (* to ensure uniqueness of env *)
    List.map env f.(fn_params) = f.(fn_sig).(sig_args) ->
    wt_stmt env f.(fn_sig).(sig_res) f.(fn_body) ->
    wt_function env f.

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

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

Soundness of type inference

Lemma expect_incr: forall te e t1 t2 e',
  expect e t1 t2 = OK e' -> S.satisf te e' -> S.satisf te e.
Global Hint Resolve expect_incr: ty.

Lemma expect_sound: forall e t1 t2 e',
  expect e t1 t2 = OK e' -> t1 = t2.

Lemma type_expr_incr: forall te a t e e',
  type_expr e a t = OK e' -> S.satisf te e' -> S.satisf te e.
Global Hint Resolve type_expr_incr: ty.

Lemma type_expr_sound: forall te a t e e',
    type_expr e a t = OK e' -> S.satisf te e' -> wt_expr te a t.

Lemma type_exprlist_incr: forall te al tl e e',
  type_exprlist e al tl = OK e' -> S.satisf te e' -> S.satisf te e.
Global Hint Resolve type_exprlist_incr: ty.

Lemma type_exprlist_sound: forall te al tl e e',
    type_exprlist e al tl = OK e' -> S.satisf te e' -> list_forall2 (wt_expr te) al tl.

Lemma type_assign_incr: forall te id a e e',
    type_assign e id a = OK e' -> S.satisf te e' -> S.satisf te e.
Global Hint Resolve type_assign_incr: ty.

Lemma type_assign_sound: forall te id a e e',
    type_assign e id a = OK e' -> S.satisf te e' -> wt_expr te a (te id).

Lemma opt_set_incr: forall te optid optty e e',
    opt_set e optid optty = OK e' -> S.satisf te e' -> S.satisf te e.
Global Hint Resolve opt_set_incr: ty.

Lemma opt_set_sound: forall te optid sg e e',
    opt_set e optid (proj_sig_res sg) = OK e' -> S.satisf te e' ->
    wt_opt_assign te optid sg.(sig_res).

Lemma type_stmt_incr: forall te tret s e e',
    type_stmt tret e s = OK e' -> S.satisf te e' -> S.satisf te e.
Global Hint Resolve type_stmt_incr: ty.

Lemma type_stmt_sound: forall te tret s e e',
    type_stmt tret e s = OK e' -> S.satisf te e' -> wt_stmt te tret s.

Theorem type_function_sound: forall f env,
  type_function f = OK env -> wt_function env f.

Semantic soundness of the type system

Definition wt_env (env: typenv) (e: Cminor.env) : Prop :=
  forall id v, e!id = Some v -> Val.has_type v (env id).

Definition def_env (f: function) (e: Cminor.env) : Prop :=
  forall id, In id f.(fn_params) \/ In id f.(fn_vars) -> exists v, e!id = Some v.

Inductive wt_cont_call: cont -> rettype -> Prop :=
  | wt_cont_Kstop:
      wt_cont_call Kstop Tint
  | wt_cont_Kcall: forall optid f sp e k tret env
        (WT_FN: wt_function env f)
        (WT_CONT: wt_cont env f.(fn_sig).(sig_res) k)
        (WT_ENV: wt_env env e)
        (DEF_ENV: def_env f e)
        (WT_DEST: wt_opt_assign env optid tret),
      wt_cont_call (Kcall optid f sp e k) tret

with wt_cont: typenv -> rettype -> cont -> Prop :=
  | wt_cont_Kseq: forall env tret s k,
      wt_stmt env tret s ->
      wt_cont env tret k ->
      wt_cont env tret (Kseq s k)
  | wt_cont_Kblock: forall env tret k,
      wt_cont env tret k ->
      wt_cont env tret (Kblock k)
  | wt_cont_other: forall env tret k,
      wt_cont_call k tret ->
      wt_cont env tret k.

Inductive wt_state: state -> Prop :=
  | wt_normal_state: forall f s k sp e m env
        (WT_FN: wt_function env f)
        (WT_STMT: wt_stmt env f.(fn_sig).(sig_res) s)
        (WT_CONT: wt_cont env f.(fn_sig).(sig_res) k)
        (WT_ENV: wt_env env e)
        (DEF_ENV: def_env f e),
      wt_state (State f s k sp e m)
  | wt_call_state: forall f args k m
        (WT_FD: wt_fundef f)
        (WT_ARGS: Val.has_type_list args (funsig f).(sig_args))
        (WT_CONT: wt_cont_call k (funsig f).(sig_res)),
      wt_state (Callstate f args k m)
  | wt_return_state: forall v k m tret
        (WT_RES: Val.has_type v (proj_rettype tret))
        (WT_CONT: wt_cont_call k tret),
      wt_state (Returnstate v k m).

Lemma wt_is_call_cont:
  forall env tret k, wt_cont env tret k -> is_call_cont k -> wt_cont_call k tret.

Lemma call_cont_wt:
  forall env tret k, wt_cont env tret k -> wt_cont_call (call_cont k) tret.

Lemma wt_env_assign: forall env id e v,
  wt_env env e -> Val.has_type v (env id) -> wt_env env (PTree.set id v e).

Lemma def_env_assign: forall f e id v,
  def_env f e -> def_env f (PTree.set id v e).

Lemma wt_env_set_params: forall env il vl,
  Val.has_type_list vl (map env il) -> wt_env env (set_params vl il).

Lemma def_set_params: forall id il vl,
  In id il -> exists v, PTree.get id (set_params vl il) = Some v.

Lemma wt_env_set_locals: forall env il e,
  wt_env env e -> wt_env env (set_locals il e).

Lemma def_set_locals: forall id il e,
  (exists v, PTree.get id e = Some v) \/ In id il ->
  exists v, PTree.get id (set_locals il e) = Some v.

Lemma wt_find_label: forall env tret lbl s k,
  wt_stmt env tret s -> wt_cont env tret k ->
  match find_label lbl s k with
  | Some (s', k') => wt_stmt env tret s' /\ wt_cont env tret k'
  | None => True
  end.

Section SUBJECT_REDUCTION.

Variable p: program.

Hypothesis wt_p: wt_program p.

Let ge := Genv.globalenv p.

Ltac VHT :=
  match goal with
  | [ |- Val.has_type (if Archi.ptr64 then _ else _) _] => unfold Val.has_type; destruct Archi.ptr64 eqn:?; VHT
  | [ |- Val.has_type (match ?v with _ => _ end) _] => destruct v; VHT
  | [ |- Val.has_type (Vptr _ _) Tptr ] => apply Val.Vptr_has_type
  | [ |- Val.has_type _ _ ] => exact I
  | [ |- Val.has_type (?f _ _ _ _ _) _ ] => unfold f; VHT
  | [ |- Val.has_type (?f _ _ _ _) _ ] => unfold f; VHT
  | [ |- Val.has_type (?f _ _) _ ] => unfold f; VHT
  | [ |- Val.has_type (?f _ _ _) _ ] => unfold f; VHT
  | [ |- Val.has_type (?f _) _ ] => unfold f; VHT
  | [ |- True ] => exact I
  | [ |- ?x = ?x ] => reflexivity
  | _ => idtac
  end.

Ltac VHT' :=
  match goal with
  | [ H: None = Some _ |- _ ] => discriminate
  | [ H: Some _ = Some _ |- _ ] => inv H; VHT
  | [ H: match ?x with _ => _ end = Some _ |- _ ] => destruct x; VHT'
  | [ H: ?f _ _ _ _ = Some _ |- _ ] => unfold f in H; VHT'
  | [ H: ?f _ _ _ = Some _ |- _ ] => unfold f in H; VHT'
  | [ H: ?f _ _ = Some _ |- _ ] => unfold f in H; VHT'
  | [ H: ?f _ = Some _ |- _ ] => unfold f in H; VHT'
  | _ => idtac
  end.

Lemma type_constant_sound: forall sp cst v,
  eval_constant ge sp cst = Some v ->
  Val.has_type v (type_constant cst).

Lemma type_unop_sound: forall op v1 v,
  eval_unop op v1 = Some v -> Val.has_type v (snd (type_unop op)).

Lemma type_binop_sound: forall op v1 v2 m v,
  eval_binop op v1 v2 m = Some v -> Val.has_type v (snd (type_binop op)).

Lemma wt_eval_expr: forall env sp e m a v,
  eval_expr ge sp e m a v ->
  forall t,
  wt_expr env a t ->
  wt_env env e ->
  Val.has_type v t.

Lemma wt_eval_exprlist: forall env sp e m al vl,
  eval_exprlist ge sp e m al vl ->
  forall tl,
  list_forall2 (wt_expr env) al tl ->
  wt_env env e ->
  Val.has_type_list vl tl.

Lemma wt_find_funct: forall v fd,
  Genv.find_funct ge v = Some fd -> wt_fundef fd.

Lemma subject_reduction:
  forall st1 t st2, step ge st1 t st2 ->
  forall (WT: wt_state st1), wt_state st2.

Lemma subject_reduction_star:
  forall st1 t st2, star step ge st1 t st2 ->
  forall (WT: wt_state st1), wt_state st2.

Lemma wt_initial_state:
  forall S, initial_state p S -> wt_state S.

End SUBJECT_REDUCTION.

Safe expressions

Definition known_idents := PTree.t unit.

Definition is_known (ki: known_idents) (id: ident) :=
  match ki!id with Some _ => true | None => false end.

Definition known_id (f: function) : known_idents :=
  let add (ki: known_idents) (id: ident) := PTree.set id tt ki in
  List.fold_left add f.(fn_vars)
      (List.fold_left add f.(fn_params) (PTree.empty unit)).


Definition safe_unop (op: unary_operation) : bool :=
  match op with
  | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => false
  | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => false
  | Olongoffloat | Olonguoffloat | Ofloatoflong | Ofloatoflongu => false
  | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => false
  | _ => true
  end.

Definition safe_binop (op: binary_operation) : bool :=
  match op with
  | Odiv | Odivu | Omod | Omodu => false
  | Odivl | Odivlu | Omodl | Omodlu => false
  | Ocmpl _ | Ocmplu _ => false
  | _ => true
  end.

Fixpoint safe_expr (ki: known_idents) (a: expr) : bool :=
  match a with
  | Evar v => is_known ki v
  | Econst c => true
  | Eunop op e1 => safe_unop op && safe_expr ki e1
  | Ebinop op e1 e2 => safe_binop op && safe_expr ki e1 && safe_expr ki e2
  | Eload chunk e => false
  end.


Lemma known_id_sound_1:
  forall f id x, (known_id f)!id = Some x -> In id f.(fn_params) \/ In id f.(fn_vars).

Lemma known_id_sound_2:
  forall f id, is_known (known_id f) id = true -> In id f.(fn_params) \/ In id f.(fn_vars).


Lemma eval_safe_expr:
  forall ge f sp e m a,
  def_env f e ->
  safe_expr (known_id f) a = true ->
  exists v, eval_expr ge sp e m a v.