Library Selectionproof

Correctness of instruction selection





Require Import Coqlib.

Require Import Maps.

Require Import AST.

Require Import Integers.

Require Import Floats.

Require Import Values.

Require Import Mem.

Require Import Events.

Require Import Globalenvs.

Require Import Smallstep.

Require Import Cminor.

Require Import Op.

Require Import CminorSel.

Require Import SelectOp.

Require Import Selection.

Require Import SelectOpproof.




Open Local Scope cminorsel_scope.

Correctness of the instruction selection functions for expressions





Section CMCONSTR.




Variable ge: genv.

Variable sp: val.

Variable e: env.

Variable m: mem.

Conversion of condition expressions.





Lemma negate_condexpr_correct:

  forall le a b,

  eval_condexpr ge sp e m le a b ->

  eval_condexpr ge sp e m le (negate_condexpr a) (negb b).






Scheme expr_ind2 := Induction for expr Sort Prop

  with exprlist_ind2 := Induction for exprlist Sort Prop.




Fixpoint forall_exprlist (P: expr -> Prop) (el: exprlist) {struct el}: Prop :=

  match el with

  | Enil => True

  | Econs e el' => P e /\ forall_exprlist P el'

  end.




Lemma expr_induction_principle:

  forall (P: expr -> Prop),

  (forall i : ident, P (Evar i)) ->

  (forall (o : operation) (e : exprlist),

     forall_exprlist P e -> P (Eop o e)) ->

  (forall (m : memory_chunk) (a : Op.addressing) (e : exprlist),

     forall_exprlist P e -> P (Eload m a e)) ->

  (forall (c : condexpr) (e : expr),

     P e -> forall e0 : expr, P e0 -> P (Econdition c e e0)) ->

  (forall e : expr, P e -> forall e0 : expr, P e0 -> P (Elet e e0)) ->

  (forall n : nat, P (Eletvar n)) ->

  forall e : expr, P e.






Lemma eval_base_condition_of_expr:

  forall le a v b,

  eval_expr ge sp e m le a v ->

  Val.bool_of_val v b ->

  eval_condexpr ge sp e m le 

                (CEcond (Ccompimm Cne Int.zero) (a ::: Enil))

                b.






Lemma is_compare_neq_zero_correct:

  forall c v b,

  is_compare_neq_zero c = true ->

  eval_condition c (v :: nil) = Some b ->

  Val.bool_of_val v b.






Lemma is_compare_eq_zero_correct:

  forall c v b,

  is_compare_eq_zero c = true ->

  eval_condition c (v :: nil) = Some b ->

  Val.bool_of_val v (negb b).






Lemma eval_condition_of_expr:

  forall a le v b,

  eval_expr ge sp e m le a v ->

  Val.bool_of_val v b ->

  eval_condexpr ge sp e m le (condexpr_of_expr a) b.






Lemma eval_load:

  forall le a v chunk v',

  eval_expr ge sp e m le a v ->

  Mem.loadv chunk m v = Some v' ->

  eval_expr ge sp e m le (load chunk a) v'.






Lemma eval_store:

  forall chunk a1 a2 v1 v2 f k m',

  eval_expr ge sp e m nil a1 v1 ->

  eval_expr ge sp e m nil a2 v2 ->

  Mem.storev chunk m v1 v2 = Some m' ->

  step ge (State f (store chunk a1 a2) k sp e m)

       E0 (State f Sskip k sp e m').

Correctness of instruction selection for operators





Lemma eval_sel_unop:

  forall le op a1 v1 v,

  eval_expr ge sp e m le a1 v1 ->

  eval_unop op v1 = Some v ->

  eval_expr ge sp e m le (sel_unop op a1) v.






Lemma eval_sel_binop:

  forall le op a1 a2 v1 v2 v,

  eval_expr ge sp e m le a1 v1 ->

  eval_expr ge sp e m le a2 v2 ->

  eval_binop op v1 v2 = Some v ->

  eval_expr ge sp e m le (sel_binop op a1 a2) v.






End CMCONSTR.

Semantic preservation for instruction selection.





Section PRESERVATION.




Variable prog: Cminor.program.

Let tprog := sel_program prog.

Let ge := Genv.globalenv prog.

Let tge := Genv.globalenv tprog.

Relationship between the global environments for the original CminorSel program and the generated RTL program.





Lemma symbols_preserved:

  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.






Lemma functions_translated:

  forall (v: val) (f: Cminor.fundef),

  Genv.find_funct ge v = Some f ->

  Genv.find_funct tge v = Some (sel_fundef f).






Lemma function_ptr_translated:

  forall (b: block) (f: Cminor.fundef),

  Genv.find_funct_ptr ge b = Some f ->

  Genv.find_funct_ptr tge b = Some (sel_fundef f).






Lemma sig_function_translated:

  forall f,

  funsig (sel_fundef f) = Cminor.funsig f.

Semantic preservation for expressions.





Lemma sel_expr_correct:

  forall sp e m a v,

  Cminor.eval_expr ge sp e m a v ->

  forall le,

  eval_expr tge sp e m le (sel_expr a) v.






Hint Resolve sel_expr_correct: evalexpr.




Lemma sel_exprlist_correct:

  forall sp e m a v,

  Cminor.eval_exprlist ge sp e m a v ->

  forall le,

  eval_exprlist tge sp e m le (sel_exprlist a) v.






Hint Resolve sel_exprlist_correct: evalexpr.

Semantic preservation for terminating function calls and statements.





Fixpoint sel_cont (k: Cminor.cont) : CminorSel.cont :=

  match k with

  | Cminor.Kstop => Kstop

  | Cminor.Kseq s1 k1 => Kseq (sel_stmt s1) (sel_cont k1)

  | Cminor.Kblock k1 => Kblock (sel_cont k1)

  | Cminor.Kcall id f sp e k1 =>

      Kcall id (sel_function f) sp e (sel_cont k1)

  end.




Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=

  | match_state: forall f s k s' k' sp e m,

      s' = sel_stmt s ->

      k' = sel_cont k ->

      match_states

        (Cminor.State f s k sp e m)

        (State (sel_function f) s' k' sp e m)

  | match_callstate: forall f args k k' m,

      k' = sel_cont k ->

      match_states

        (Cminor.Callstate f args k m)

        (Callstate (sel_fundef f) args k' m)

  | match_returnstate: forall v k k' m,

      k' = sel_cont k ->

      match_states

        (Cminor.Returnstate v k m)

        (Returnstate v k' m).




Remark call_cont_commut:

  forall k, call_cont (sel_cont k) = sel_cont (Cminor.call_cont k).






Remark find_label_commut:

  forall lbl s k,

  find_label lbl (sel_stmt s) (sel_cont k) =

  option_map (fun sk => (sel_stmt (fst sk), sel_cont (snd sk)))

             (Cminor.find_label lbl s k).






Lemma sel_step_correct:

  forall S1 t S2, Cminor.step ge S1 t S2 ->

  forall T1, match_states S1 T1 ->

  exists T2, step tge T1 t T2 /\ match_states S2 T2.






Lemma sel_initial_states:

  forall S, Cminor.initial_state prog S ->

  exists R, initial_state 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:

  forall (beh: program_behavior), not_wrong beh ->

  Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh.






End PRESERVATION.