diff options
Diffstat (limited to 'backend/Selectionproof.v')
-rw-r--r-- | backend/Selectionproof.v | 52 |
1 files changed, 50 insertions, 2 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index bb9bd592..d755d46d 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -520,6 +520,14 @@ Proof. auto. Qed. +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). +Proof. + unfold set_optvar; intros. destruct optid; auto. apply set_var_lessdef; auto. +Qed. + Lemma set_params_lessdef: forall il vl1 vl2, Val.lessdef_list vl1 vl2 -> @@ -590,6 +598,25 @@ Proof. exists (v1' :: vl'); split; auto. constructor; eauto. Qed. +Lemma sel_annot_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 -> + exists vl', + list_forall2 (CminorSel.eval_annot_arg tge sp e' m') + (List.map (fun a => annot_arg (sel_expr a)) al) + vl' + /\ Val.lessdef_list vl vl'. +Proof. + induction 3; simpl. +- exists (@nil val); split; constructor. +- exploit sel_expr_correct; eauto. intros (v1' & A & B). + destruct IHeval_exprlist as (vl' & C & D). + exists (v1' :: vl'); split; auto. + constructor; auto. eapply eval_annot_arg; eauto. +Qed. + (** Semantic preservation for functions and statements. *) Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop := @@ -675,6 +702,8 @@ Proof. destruct (classify_call ge e); simpl; auto. (* tailcall *) destruct (classify_call ge e); simpl; auto. +(* builtin *) + destruct (builtin_is_annot e); simpl; auto. (* seq *) exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ]; @@ -776,14 +805,33 @@ Proof. econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto. constructor; auto. apply call_cont_commut; auto. - (* Sbuiltin *) + destruct (builtin_is_annot ef optid) eqn:ISANNOT. ++ (* annotation *) + assert (X: exists text targs, ef = EF_annot text targs). + { destruct ef; try discriminate. econstructor; econstructor; eauto. } + destruct X as (text & targs & EQ). + assert (Y: optid = None). + { destruct ef; try discriminate. destruct optid; try discriminate. auto. } + exploit sel_annot_args_correct; eauto. + set (bl' := map (fun e => annot_arg (sel_expr e)) bl). + intros (vargs' & P & Q). + exploit external_call_mem_extends; eauto. + intros [vres' [m2 [A [B [C D]]]]]. + left; econstructor; split. + econstructor. + rewrite EQ; auto. + eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + rewrite Y. constructor; auto. ++ (* other builtin *) exploit sel_exprlist_correct; eauto. intros [vargs' [P Q]]. exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - constructor; auto. - destruct optid; simpl; auto. apply set_var_lessdef; auto. + constructor; auto. apply set_optvar_lessdef; auto. - (* Seq *) left; econstructor; split. constructor. constructor; auto. constructor; auto. |