Require Import Coqlib Maps.
Require Import AST Linking Errors Integers Values Memory Events Globalenvs Smallstep.
Require Import Switch Cminor Op CminorSel.
Require Import SelectOp SelectDiv SplitLong SelectLong Selection.
Require Import SelectOpproof SelectDivproof SplitLongproof SelectLongproof.

Local Open Scope cminorsel_scope.
Local Open Scope error_monad_scope.

Relational specification of instruction selection

Definition match_fundef (cunit: Cminor.program) (f: Cminor.fundef) (tf: CminorSel.fundef) : Prop :=
  exists hf, helper_functions_declared cunit hf /\ sel_fundef (prog_defmap cunit) hf f = OK tf.

Definition match_prog (p: Cminor.program) (tp: CminorSel.program) :=
  match_program match_fundef eq p tp.


Lemma record_globdefs_sound:
  forall dm id gd, (record_globdefs dm)!id = Some gd -> dm!id = Some gd.

Lemma lookup_helper_correct_1:
  forall globs name sg id,
  lookup_helper globs name sg = OK id ->
  globs!id = Some (Gfun (External (EF_runtime name sg))).

Lemma lookup_helper_correct:
  forall p name sg id,
  lookup_helper (record_globdefs (prog_defmap p)) name sg = OK id ->
  helper_declared p id name sg.

Lemma get_helpers_correct:
  forall p hf,
  get_helpers (prog_defmap p) = OK hf -> helper_functions_declared p hf.

Theorem transf_program_match:
  forall p tp, sel_program p = OK tp -> match_prog p tp.

Lemma helper_functions_declared_linkorder:
  forall (p p': Cminor.program) hf,
  helper_functions_declared p hf -> linkorder p p' -> helper_functions_declared p' hf.

Correctness of the instruction selection functions for expressions

Section PRESERVATION.
  Existing Instance inject_perm_all.

Variable fn_stack_requirements: ident -> Z.
Context `{external_calls_prf: ExternalCalls}.
Context `{i64_helpers_correct_prf: !I64HelpersCorrect mem}.

Variable prog: Cminor.program.
Variable tprog: CminorSel.program.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.
Hypothesis TRANSF: match_prog prog tprog.

Lemma symbols_preserved:
  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_match TRANSF).

Lemma senv_preserved:
  Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
Proof (Genv.senv_match TRANSF).

Lemma genv_next_preserved:
  Genv.genv_next tge = Genv.genv_next ge.

Lemma function_ptr_translated:
  forall (b: block) (f: Cminor.fundef),
  Genv.find_funct_ptr ge b = Some f ->
  exists cu tf, Genv.find_funct_ptr tge b = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.
Proof (Genv.find_funct_ptr_match TRANSF).

Lemma functions_translated:
  forall (v v': val) (f: Cminor.fundef),
  Genv.find_funct ge v = Some f ->
  Val.lessdef v v' ->
  exists cu tf, Genv.find_funct tge v' = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.

Lemma sig_function_translated:
  forall cu f tf, match_fundef cu f tf -> funsig tf = Cminor.funsig f.

Lemma stackspace_function_translated:
  forall dm hf f tf, sel_function dm hf f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f.

Lemma helper_functions_preserved:
  forall hf, helper_functions_declared prog hf -> helper_functions_declared tprog hf.

Section CMCONSTR.

Variable cunit: Cminor.program.
Variable hf: helper_functions.
Hypothesis LINK: linkorder cunit prog.
Hypothesis HF: helper_functions_declared cunit hf.

Let HF': helper_functions_declared tprog hf.

Variable sp: val.
Variable e: env.
Variable m: mem.

Lemma eval_condexpr_of_expr:
  forall a le v b,
  eval_expr tge sp e m le a v ->
  Val.bool_of_val v b ->
  eval_condexpr tge sp e m le (condexpr_of_expr a) b.

Lemma eval_load:
  forall le a v chunk v',
  eval_expr tge sp e m le a v ->
  Mem.loadv chunk m v = Some v' ->
  eval_expr tge sp e m le (load chunk a) v'.

Lemma eval_store:
  forall chunk a1 a2 v1 v2 f k m',
  eval_expr tge sp e m nil a1 v1 ->
  eval_expr tge sp e m nil a2 v2 ->
  Mem.storev chunk m v1 v2 = Some m' ->
  step fn_stack_requirements tge (State f (store chunk a1 a2) k sp e m)
        E0 (State f Sskip k sp e m').


Lemma eval_sel_unop:
  forall le op a1 v1 v,
  eval_expr tge sp e m le a1 v1 ->
  eval_unop op v1 = Some v ->
  exists v', eval_expr tge sp e m le (sel_unop op a1) v' /\ Val.lessdef v v'.

Lemma eval_sel_binop:
  forall le op a1 a2 v1 v2 v,
  eval_expr tge sp e m le a1 v1 ->
  eval_expr tge sp e m le a2 v2 ->
  eval_binop op v1 v2 m = Some v ->
  exists v', eval_expr tge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'.

End CMCONSTR.


Lemma expr_is_addrof_ident_correct:
  forall e id,
  expr_is_addrof_ident e = Some id ->
  e = Cminor.Econst (Cminor.Oaddrsymbol id Ptrofs.zero).

Lemma ef_inline_enabled:
  forall ef,
    ef_inline ef = true ->
    builtin_enabled ef.
Hint Resolve ef_inline_enabled.

Lemma classify_call_correct:
  forall unit sp e m a v fd,
  linkorder unit prog ->
  Cminor.eval_expr ge sp e m a v ->
  Genv.find_funct ge v = Some fd ->
  match classify_call (prog_defmap unit) a with
  | Call_default => True
  | Call_imm id => exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b Ptrofs.zero
  | Call_builtin ef => fd = External ef /\ builtin_enabled ef
  end.


Inductive Rint: Z -> val -> Prop :=
  | Rint_intro: forall n, Rint (Int.unsigned n) (Vint n).

Inductive Rlong: Z -> val -> Prop :=
  | Rlong_intro: forall n, Rlong (Int64.unsigned n) (Vlong n).

Section SEL_SWITCH.

Variable make_cmp_eq: expr -> Z -> expr.
Variable make_cmp_ltu: expr -> Z -> expr.
Variable make_sub: expr -> Z -> expr.
Variable make_to_int: expr -> expr.
Variable modulus: Z.
Variable R: Z -> val -> Prop.

Hypothesis eval_make_cmp_eq: forall sp e m le a v i n,
  eval_expr tge sp e m le a v -> R i v -> 0 <= n < modulus ->
  eval_expr tge sp e m le (make_cmp_eq a n) (Val.of_bool (zeq i n)).
Hypothesis eval_make_cmp_ltu: forall sp e m le a v i n,
  eval_expr tge sp e m le a v -> R i v -> 0 <= n < modulus ->
  eval_expr tge sp e m le (make_cmp_ltu a n) (Val.of_bool (zlt i n)).
Hypothesis eval_make_sub: forall sp e m le a v i n,
  eval_expr tge sp e m le a v -> R i v -> 0 <= n < modulus ->
  exists v', eval_expr tge sp e m le (make_sub a n) v' /\ R ((i - n) mod modulus) v'.
Hypothesis eval_make_to_int: forall sp e m le a v i,
  eval_expr tge sp e m le a v -> R i v ->
  exists v', eval_expr tge sp e m le (make_to_int a) v' /\ Rint (i mod Int.modulus) v'.

Lemma sel_switch_correct_rec:
  forall sp e m varg i x,
  R i varg ->
  forall t arg le,
  wf_comptree modulus t ->
  nth_error le arg = Some varg ->
  comptree_match modulus i t = Some x ->
  eval_exitexpr tge sp e m le (sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int arg t) x.

Lemma sel_switch_correct:
  forall dfl cases arg sp e m varg i t le,
  validate_switch modulus dfl cases t = true ->
  eval_expr tge sp e m le arg varg ->
  R i varg ->
  0 <= i < modulus ->
  eval_exitexpr tge sp e m le
     (XElet arg (sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int O t))
     (switch_target i dfl cases).

End SEL_SWITCH.

Lemma sel_switch_int_correct:
  forall dfl cases arg sp e m i t le,
  validate_switch Int.modulus dfl cases t = true ->
  eval_expr tge sp e m le arg (Vint i) ->
  eval_exitexpr tge sp e m le (XElet arg (sel_switch_int O t)) (switch_target (Int.unsigned i) dfl cases).

Lemma sel_switch_long_correct:
  forall dfl cases arg sp e m i t le,
  validate_switch Int64.modulus dfl cases t = true ->
  eval_expr tge sp e m le arg (Vlong i) ->
  eval_exitexpr tge sp e m le (XElet arg (sel_switch_long O t)) (switch_target (Int64.unsigned i) dfl cases).


Ltac TrivialExists :=
  match goal with
  | [ |- exists v, Some ?x = Some v /\ _ ] => exists x; split; auto
  | _ => idtac
  end.

Lemma eval_unop_lessdef:
  forall op v1 v1' v,
  eval_unop op v1 = Some v -> Val.lessdef v1 v1' ->
  exists v', eval_unop op v1' = Some v' /\ Val.lessdef v v'.

Lemma eval_binop_lessdef:
  forall op v1 v1' v2 v2' v m m',
  eval_binop op v1 v2 m = Some v ->
  Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Mem.extends m m' ->
  exists v', eval_binop op v1' v2' m' = Some v' /\ Val.lessdef v v'.

Semantic preservation for instruction selection.

Definition env_lessdef (e1 e2: env) : Prop :=
  forall id v1, e1!id = Some v1 -> exists v2, e2!id = Some v2 /\ Val.lessdef v1 v2.

Lemma set_var_lessdef:
  forall e1 e2 id v1 v2,
  env_lessdef e1 e2 -> Val.lessdef v1 v2 ->
  env_lessdef (PTree.set id v1 e1) (PTree.set id v2 e2).

Lemma set_optvar_lessdef:
  forall e1 e2 optid v1 v2,
  env_lessdef e1 e2 -> Val.lessdef v1 v2 ->
  env_lessdef (set_optvar optid v1 e1) (set_optvar optid v2 e2).

Lemma set_params_lessdef:
  forall il vl1 vl2,
  Val.lessdef_list vl1 vl2 ->
  env_lessdef (set_params vl1 il) (set_params vl2 il).

Lemma set_locals_lessdef:
  forall e1 e2, env_lessdef e1 e2 ->
  forall il, env_lessdef (set_locals il e1) (set_locals il e2).


Section EXPRESSIONS.

Variable cunit: Cminor.program.
Variable hf: helper_functions.
Hypothesis LINK: linkorder cunit prog.
Hypothesis HF: helper_functions_declared cunit hf.

Lemma sel_expr_correct:
  forall sp e m a v,
  Cminor.eval_expr ge sp e m a v ->
  forall e' le m',
  env_lessdef e e' -> Mem.extends m m' ->
  exists v', eval_expr tge sp e' m' le (sel_expr a) v' /\ Val.lessdef v v'.

Lemma sel_exprlist_correct:
  forall sp e m a v,
  Cminor.eval_exprlist ge sp e m a v ->
  forall e' le m',
  env_lessdef e e' -> Mem.extends m m' ->
  exists v', eval_exprlist tge sp e' m' le (sel_exprlist a) v' /\ Val.lessdef_list v v'.

Lemma sel_builtin_arg_correct:
  forall sp e e' m m' a v c,
  env_lessdef e e' -> Mem.extends m m' ->
  Cminor.eval_expr ge sp e m a v ->
  exists v',
     CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg a c) v'
  /\ Val.lessdef v v'.

Lemma sel_builtin_args_correct:
  forall sp e e' m m',
  env_lessdef e e' -> Mem.extends m m' ->
  forall al vl,
  Cminor.eval_exprlist ge sp e m al vl ->
  forall cl,
  exists vl',
     list_forall2 (CminorSel.eval_builtin_arg tge sp e' m')
                  (sel_builtin_args al cl)
                  vl'
  /\ Val.lessdef_list vl vl'.

Lemma sel_builtin_res_correct:
  forall oid v e v' e',
  env_lessdef e e' -> Val.lessdef v v' ->
  env_lessdef (set_optvar oid v e) (set_builtin_res (sel_builtin_res oid) v' e').

End EXPRESSIONS.


Inductive match_cont: Cminor.program -> helper_functions -> Cminor.cont -> CminorSel.cont -> Prop :=
  | match_cont_stop: forall cunit hf,
      match_cont cunit hf Cminor.Kstop Kstop
  | match_cont_seq: forall cunit hf s s' k k',
      sel_stmt (prog_defmap cunit) s = OK s' ->
      match_cont cunit hf k k' ->
      match_cont cunit hf (Cminor.Kseq s k) (Kseq s' k')
  | match_cont_block: forall cunit hf k k',
      match_cont cunit hf k k' ->
      match_cont cunit hf (Cminor.Kblock k) (Kblock k')
  | match_cont_call: forall cunit' hf' cunit hf id f sp e k f' e' k',
      linkorder cunit prog ->
      helper_functions_declared cunit hf ->
      sel_function (prog_defmap cunit) hf f = OK f' ->
      match_cont cunit hf k k' -> env_lessdef e e' ->
      match_cont cunit' hf' (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k').

Definition match_call_cont (k: Cminor.cont) (k': CminorSel.cont) : Prop :=
  forall cunit hf, match_cont cunit hf k k'.

Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
  | match_state: forall cunit hf f f' s k s' k' sp e m e' m'
        (LINK: linkorder cunit prog)
        (HF: helper_functions_declared cunit hf)
        (TF: sel_function (prog_defmap cunit) hf f = OK f')
        (TS: sel_stmt (prog_defmap cunit) s = OK s')
        (MC: match_cont cunit hf k k')
        (LD: env_lessdef e e')
        (ME: Mem.extends m m')
        (STRUCT: stack_equiv (Mem.stack m) (Mem.stack m')),
      match_states
        (Cminor.State f s k sp e m)
        (State f' s' k' sp e' m')
  | match_callstate: forall cunit f f' args args' k k' m m' sz
        (LINK: linkorder cunit prog)
        (TF: match_fundef cunit f f')
        (MC: match_call_cont k k')
        (LD: Val.lessdef_list args args')
        (ME: Mem.extends m m')
        (STRUCT: stack_equiv (Mem.stack m) (Mem.stack m')),
      match_states
        (Cminor.Callstate f args k m sz)
        (Callstate f' args' k' m' sz)
  | match_returnstate: forall v v' k k' m m'
        (MC: match_call_cont k k')
        (LD: Val.lessdef v v')
        (ME: Mem.extends m m')
        (STRUCT: stack_equiv (Mem.stack m) (Mem.stack m')),
      match_states
        (Cminor.Returnstate v k m)
        (Returnstate v' k' m')
  | match_builtin_1: forall cunit hf ef args args' optid f sp e k m al f' e' k' m' sz
        (LINK: linkorder cunit prog)
        (HF: helper_functions_declared cunit hf)
        (TF: sel_function (prog_defmap cunit) hf f = OK f')
        (MC: match_cont cunit hf k k')
        (LDA: Val.lessdef_list args args')
        (LDE: env_lessdef e e')
        (ME: Mem.extends m m')
        (STRUCT: stack_equiv (Mem.stack m) (Mem.stack m'))
        (EA: list_forall2 (CminorSel.eval_builtin_arg tge sp e' m') al args'),
      forall BUILTIN_ENABLED : builtin_enabled ef,
        match_states
          (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) (Mem.push_new_stage m) sz)
          (State f' (Sbuiltin (sel_builtin_res optid) ef al) k' sp e' m')
  | match_builtin_2: forall cunit hf v v' optid f sp e k m f' e' m' k'
        (LINK: linkorder cunit prog)
        (HF: helper_functions_declared cunit hf)
        (TF: sel_function (prog_defmap cunit) hf f = OK f')
        (MC: match_cont cunit hf k k')
        (LDV: Val.lessdef v v')
        (LDE: env_lessdef e e')
        (ME: forall m'', Mem.unrecord_stack_block m = Some m'' -> Mem.extends m'' m')
        (STRUCT: stack_equiv (tl (Mem.stack m)) (Mem.stack m')),
      match_states
        (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m)
        (State f' Sskip k' sp (set_builtin_res (sel_builtin_res optid) v' e') m').

Remark call_cont_commut:
  forall cunit hf k k', match_cont cunit hf k k' -> match_call_cont (Cminor.call_cont k) (call_cont k').

Remark match_is_call_cont:
  forall cunit hf k k', match_cont cunit hf k k' -> Cminor.is_call_cont k -> match_call_cont k k'.

Remark match_call_cont_cont:
  forall k k', match_call_cont k k' -> exists cunit hf, match_cont cunit hf k k'.

Remark find_label_commut:
  forall cunit hf lbl s k s' k',
  match_cont cunit hf k k' ->
  sel_stmt (prog_defmap cunit) s = OK s' ->
  match Cminor.find_label lbl s k, find_label lbl s' k' with
  | None, None => True
  | Some(s1, k1), Some(s1', k1') => sel_stmt (prog_defmap cunit) s1 = OK s1' /\ match_cont cunit hf k1 k1'
  | _, _ => False
  end.

Definition measure (s: Cminor.state) : nat :=
  match s with
  | Cminor.Callstate _ _ _ _ _ => 0%nat
  | Cminor.State _ _ _ _ _ _ => 1%nat
  | Cminor.Returnstate _ _ _ => 2%nat
  end.

Lemma sel_step_correct:
  forall S1 t S2, Cminor.step fn_stack_requirements ge S1 t S2 ->
  forall T1, match_states S1 T1 -> stack_inv T1 ->
  (exists T2, step fn_stack_requirements tge T1 t T2 /\ match_states S2 T2)
  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat.

Lemma sel_initial_states:
  forall S, Cminor.initial_state fn_stack_requirements prog S ->
  exists R, initial_state fn_stack_requirements tprog R /\ match_states S R.

Lemma sel_final_states:
  forall S R r,
  match_states S R -> Cminor.final_state S r -> final_state R r.

Theorem transf_program_correct:
  forward_simulation (Cminor.semantics fn_stack_requirements prog) (CminorSel.semantics fn_stack_requirements tprog).

End PRESERVATION.

Commutation with linking

Instance TransfSelectionLink : TransfLink match_prog.