From 4622f49fd089ae47d0c853343cb0a05f986c962a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 27 Mar 2015 08:55:05 +0100 Subject: Extend annotations so that they can keep track of global variables and local variables whose address is taken. - CminorSel, RTL: add "annot" instructions. - CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions. - AST, Events: simplify EF_annot because constants are now part of the arguments. Implementation is not complete yet. --- backend/CSEproof.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'backend/CSEproof.v') diff --git a/backend/CSEproof.v b/backend/CSEproof.v index ae8052be..74e3ceca 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -1144,6 +1144,21 @@ Proof. + apply CASE1. * apply set_reg_lessdef; auto. +- (* Iannot *) + exploit (@eval_annot_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto. + intros (vargs' & A & B). + exploit external_call_mem_extends; eauto. + intros (v' & m1' & P & Q & R & S). + econstructor; split. + 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. + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. replace m' with m; auto. + destruct ef; try contradiction. inv H2; auto. + - (* Icond *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. elim SAT; intros valu1 NH1. -- cgit