diff options
Diffstat (limited to 'backend/RTLgenproof.v')
| -rw-r--r-- | backend/RTLgenproof.v | 247 |
1 files changed, 247 insertions, 0 deletions
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 8acce510..02460f67 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -972,6 +972,234 @@ Proof. auto. Qed. +(** Annotation arguments. *) + +Lemma eval_exprlist_append: + forall le al1 vl1 al2 vl2, + eval_exprlist ge sp e m le (exprlist_of_expr_list al1) vl1 -> + eval_exprlist ge sp e m le (exprlist_of_expr_list al2) vl2 -> + eval_exprlist ge sp e m le (exprlist_of_expr_list (al1 ++ al2)) (vl1 ++ vl2). +Proof. + induction al1; simpl; intros vl1 al2 vl2 E1 E2; inv E1. +- auto. +- simpl. constructor; eauto. +Qed. + +Lemma invert_eval_annot_arg: + forall a v, + eval_annot_arg ge sp e m a v -> + exists vl, + eval_exprlist ge sp e m nil (exprlist_of_expr_list (params_of_annot_arg a)) vl + /\ Events.eval_annot_arg ge (fun v => v) sp m (fst (convert_annot_arg a vl)) v + /\ (forall vl', convert_annot_arg a (vl ++ vl') = (fst (convert_annot_arg a vl), vl')). +Proof. + induction 1; simpl; econstructor; intuition eauto with evalexpr aarg. + constructor. + constructor. + repeat constructor. +Qed. + +Lemma invert_eval_annot_args: + forall al vl, + list_forall2 (eval_annot_arg ge sp e m) al vl -> + exists vl', + eval_exprlist ge sp e m nil (exprlist_of_expr_list (params_of_annot_args al)) vl' + /\ Events.eval_annot_args ge (fun v => v) sp m (convert_annot_args al vl') vl. +Proof. + induction 1; simpl. +- exists (@nil val); split; constructor. +- exploit invert_eval_annot_arg; eauto. intros (vl1 & A & B & C). + destruct IHlist_forall2 as (vl2 & D & E). + exists (vl1 ++ vl2); split. + apply eval_exprlist_append; auto. + rewrite C; simpl. constructor; auto. +Qed. + +Lemma transl_eval_annot_arg: + forall rs a vl rl v, + Val.lessdef_list vl rs##rl -> + Events.eval_annot_arg ge (fun v => v) sp m (fst (convert_annot_arg a vl)) v -> + exists v', + Events.eval_annot_arg ge (fun r => rs#r) sp m (fst (convert_annot_arg a rl)) v' + /\ Val.lessdef v v' + /\ Val.lessdef_list (snd (convert_annot_arg a vl)) rs##(snd (convert_annot_arg a rl)). +Proof. + induction a; simpl; intros until v; intros LD EV; + try (now (inv EV; econstructor; eauto with aarg)). +- destruct rl; simpl in LD; inv LD; inv EV; simpl. + econstructor; eauto with aarg. + exists (rs#p); intuition auto. constructor. +- destruct (convert_annot_arg a1 vl) as [a1' vl1] eqn:CV1; simpl in *. + destruct (convert_annot_arg a2 vl1) as [a2' vl2] eqn:CV2; simpl in *. + destruct (convert_annot_arg a1 rl) as [a1'' rl1] eqn:CV3; simpl in *. + destruct (convert_annot_arg a2 rl1) as [a2'' rl2] eqn:CV4; simpl in *. + inv EV. + exploit IHa1; eauto. rewrite CV1; simpl; eauto. + rewrite CV1, CV3; simpl. intros (v1' & A1 & B1 & C1). + exploit IHa2. eexact C1. rewrite CV2; simpl; eauto. + rewrite CV2, CV4; simpl. intros (v2' & A2 & B2 & C2). + exists (Val.longofwords v1' v2'); split. constructor; auto. + split; auto. apply Val.longofwords_lessdef; auto. +Qed. + +Lemma transl_eval_annot_args: + forall rs al vl1 rl vl, + Val.lessdef_list vl1 rs##rl -> + Events.eval_annot_args ge (fun v => v) sp m (convert_annot_args al vl1) vl -> + exists vl', + Events.eval_annot_args ge (fun r => rs#r) sp m (convert_annot_args al rl) vl' + /\ Val.lessdef_list vl vl'. +Proof. + induction al; simpl; intros until vl; intros LD EV. +- inv EV. exists (@nil val); split; constructor. +- destruct (convert_annot_arg a vl1) as [a1' vl2] eqn:CV1; simpl in *. + inv EV. + exploit transl_eval_annot_arg. eauto. instantiate (2 := a). rewrite CV1; simpl; eauto. + rewrite CV1; simpl. intros (v1' & A1 & B1 & C1). + exploit IHal. eexact C1. eauto. intros (vl' & A2 & B2). + destruct (convert_annot_arg a rl) as [a1'' rl2]; simpl in *. + exists (v1' :: vl'); split; constructor; auto. +Qed. + + +(* +Definition transl_annot_arg_prop (a: annot_arg expr) (v: val): Prop := + forall tm cs f map pr ns nd a' rs + (MWF: map_wf map) + (TR: tr_annot_arg f.(fn_code) map pr a ns nd a') + (ME: match_env map e nil rs) + (EXT: Mem.extends m tm), + exists rs', exists tm', exists v', + star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm') + /\ match_env map e nil rs' + /\ Events.eval_annot_arg tge (fun r => rs'#r) sp tm' a' v' + /\ Val.lessdef v v' + /\ (forall r, In r pr -> rs'#r = rs#r) + /\ Mem.extends m tm'. + +Theorem transl_annot_arg_correct: + forall a v, + eval_annot_arg ge sp e m a v -> + transl_annot_arg_prop a v. +Proof. + induction 1; red; intros; inv TR. +- exploit transl_expr_correct; eauto. intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1). + exists rs1, tm1, rs1#r; intuition eauto. constructor. +- exists rs, tm, (Vint n); intuition auto using star_refl with aarg. +- exists rs, tm, (Vlong n); intuition auto using star_refl with aarg. +- exists rs, tm, (Vfloat n); intuition auto using star_refl with aarg. +- exists rs, tm, (Vsingle n); intuition auto using star_refl with aarg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). + exists rs, tm, v'; intuition auto using star_refl with aarg. +- exists rs, tm, (Val.add sp (Vint ofs)); intuition auto using star_refl with aarg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). + replace (Genv.symbol_address ge id ofs) + with (Senv.symbol_address tge id ofs) in P. + exists rs, tm, v'; intuition auto using star_refl with aarg. + unfold Genv.symbol_address, Senv.symbol_address. simpl. + rewrite symbols_preserved; auto. +- exists rs, tm, (Senv.symbol_address tge id ofs); intuition auto using star_refl with aarg. + unfold Genv.symbol_address, Senv.symbol_address. simpl. + rewrite symbols_preserved; auto. +- inv H5. inv H9. simpl in H5. + exploit transl_expr_correct. eexact H. eauto. eauto. eauto. eauto. + intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1). + exploit transl_expr_correct. eexact H0. eauto. eauto. eauto. eauto. + intros (rs2 & tm2 & A2 & B2 & C2 & D2 & E2). + exists rs2, tm2, (Val.longofwords rs2#r rs2#r0); intuition auto. + eapply star_trans; eauto. + constructor. constructor. constructor. + rewrite (D2 r) by auto with coqlib. apply Val.longofwords_lessdef; auto. + transitivity rs1#r1; auto with coqlib. +Qed. + + +Definition transl_annot_args_prop (l: list (annot_arg expr)) (vl: list val): Prop := + forall tm cs f map pr ns nd l' rs + (MWF: map_wf map) + (TR: tr_annot_args f.(fn_code) map pr l ns nd l') + (ME: match_env map e nil rs) + (EXT: Mem.extends m tm), + exists rs', exists tm', exists vl', + star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm') + /\ match_env map e nil rs' + /\ eval_annot_args tge (fun r => rs'#r) sp tm' l' vl' + /\ Val.lessdef_list vl vl' + /\ (forall r, In r pr -> rs'#r = rs#r) + /\ Mem.extends m tm'. + +Theorem transl_annot_args_correct: + forall l vl, + list_forall2 (eval_annot_arg ge sp e m) l vl -> + transl_annot_args_prop l vl. +Proof. + induction 1; red; intros. +- inv TR. exists rs, tm, (@nil val). + split. constructor. + split. auto. + split. constructor. + split. constructor. + split. auto. + auto. +- inv TR. inv H; inv H5. + + exploit transl_expr_correct; eauto. + intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1). + exploit (IHlist_forall2 tm1 cs); eauto. + intros (rs2 & tm2 & vl2 & A2 & B2 & C2 & D2 & E2 & F2). simpl in E2. + exists rs2, tm2, (rs2#r :: vl2); intuition auto. + eapply star_trans; eauto. + constructor; auto. constructor. + rewrite E2; auto. + transitivity rs1#r0; auto. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Vint n :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Vlong n :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Vfloat n :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Vsingle n :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exploit Mem.loadv_extends; eauto. intros (v1' & P & Q). + exists rs', tm', (v1' :: vl'); simpl; intuition auto. constructor; eauto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Val.add sp (Vint ofs) :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exploit Mem.loadv_extends; eauto. intros (v1' & P & Q). + replace (Genv.symbol_address ge id ofs) + with (Senv.symbol_address tge id ofs) in P. + exists rs', tm', (v1' :: vl'); simpl; intuition auto. constructor; auto with aarg. + unfold Genv.symbol_address, Senv.symbol_address. simpl. + rewrite symbols_preserved; auto. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Genv.symbol_address tge id ofs :: vl'); simpl; intuition auto. + constructor; auto with aarg. constructor. + unfold Genv.symbol_address. rewrite symbols_preserved; auto. + + inv H7. inv H12. + exploit transl_expr_correct. eexact H1. eauto. eauto. eauto. eauto. + intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1). + exploit transl_expr_correct. eexact H2. eauto. eauto. eauto. eexact E1. + intros (rs2 & tm2 & A2 & B2 & C2 & D2 & E2). simpl in D2. + exploit (IHlist_forall2 tm2 cs); eauto. + intros (rs3 & tm3 & vl3 & A3 & B3 & C3 & D3 & E3 & F3). simpl in E3. + exists rs3, tm3, (Val.longofwords rs3#r rs3#r0 :: vl3); intuition auto. + eapply star_trans; eauto. eapply star_trans; eauto. auto. + constructor; auto with aarg. constructor. constructor. constructor. + constructor; auto. apply Val.longofwords_lessdef. + rewrite E3, D2; auto. + rewrite E3; auto. + transitivity rs1#r1; auto. transitivity rs2#r1; auto. +Qed. +*) + End CORRECTNESS_EXPR. (** ** Measure over CminorSel states *) @@ -1304,6 +1532,25 @@ Proof. econstructor; eauto. constructor. eapply match_env_update_dest; eauto. + (* annot *) + inv TS. exploit invert_eval_annot_args; eauto. intros (vparams & P & Q). + exploit transl_exprlist_correct; eauto. + intros [rs' [tm' [E [F [G [J K]]]]]]. + exploit transl_eval_annot_args; eauto. + intros (vargs' & U & V). + exploit (@eval_annot_args_lessdef _ ge (fun r => rs'#r) (fun r => rs'#r)); eauto. + intros (vargs'' & X & Y). + assert (Z: Val.lessdef_list vl vargs'') by (eapply Val.lessdef_list_trans; eauto). + edestruct external_call_mem_extends as [tv [tm'' [A [B [C D]]]]]; eauto. + econstructor; split. + left. eapply plus_right. eexact E. + eapply exec_Iannot; eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved. eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + traceEq. + econstructor; eauto. constructor. + (* seq *) inv TS. econstructor; split. |