From 202bc495442a1a8fa184b73ac0063bdbbbcdf846 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 24 Feb 2013 09:01:28 +0000 Subject: Constant propagation within __builtin_annot. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/CMparser.mly | 3 +- backend/Constprop.v | 39 ++++++++++++++++++++++++- backend/Constpropproof.v | 74 ++++++++++++++++++++++++++++++++++++++++++---- backend/PrintAnnot.ml | 76 ++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 185 insertions(+), 7 deletions(-) create mode 100644 backend/PrintAnnot.ml (limited to 'backend') diff --git a/backend/CMparser.mly b/backend/CMparser.mly index eb3b9ab..273d572 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -55,7 +55,8 @@ let mkef sg toks = | [EFT_tok "memcpy"; EFT_tok "size"; EFT_int sz; EFT_tok "align"; EFT_int al] -> EF_memcpy(Z.of_sint32 sz, Z.of_sint32 al) | [EFT_tok "annot"; EFT_string txt] -> - EF_annot(intern_string txt, sg.sig_args) + EF_annot(intern_string txt, + List.map (fun t -> AA_arg t) sg.sig_args) | [EFT_tok "annot_val"; EFT_string txt] -> if sg.sig_args = [] then raise Parsing.Parse_error; EF_annot_val(intern_string txt, List.hd sg.sig_args) diff --git a/backend/Constprop.v b/backend/Constprop.v index fe16240..8fa0691 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -296,6 +296,43 @@ Definition num_iter := 10%nat. Definition successor (f: function) (app: D.t) (pc: node) : node := successor_rec num_iter f app pc. +Function annot_strength_reduction + (app: D.t) (targs: list annot_arg) (args: list reg) := + match targs, args with + | AA_arg ty :: targs', arg :: args' => + let (targs'', args'') := annot_strength_reduction app targs' args' in + match ty, approx_reg app arg with + | Tint, I n => (AA_int n :: targs'', args'') + | Tfloat, F n => (AA_float n :: targs'', args'') + | _, _ => (AA_arg ty :: targs'', arg :: args'') + end + | targ :: targs', _ => + let (targs'', args'') := annot_strength_reduction app targs' args in + (targ :: targs'', args'') + | _, _ => + (targs, args) + end. + +Function builtin_strength_reduction + (app: D.t) (ef: external_function) (args: list reg) := + match ef, args with + | EF_vload chunk, r1 :: nil => + match approx_reg app r1 with + | G symb n1 => (EF_vload_global chunk symb n1, nil) + | _ => (ef, args) + end + | EF_vstore chunk, r1 :: r2 :: nil => + match approx_reg app r1 with + | G symb n1 => (EF_vstore_global chunk symb n1, r2 :: nil) + | _ => (ef, args) + end + | EF_annot text targs, args => + let (targs', args') := annot_strength_reduction app targs args in + (EF_annot text targs', args') + | _, _ => + (ef, args) + end. + Definition transf_instr (gapp: global_approx) (f: function) (apps: PMap.t D.t) (pc: node) (instr: instruction) := let app := apps!!pc in @@ -328,7 +365,7 @@ Definition transf_instr (gapp: global_approx) (f: function) (apps: PMap.t D.t) | Itailcall sig ros args => Itailcall sig (transf_ros app ros) args | Ibuiltin ef args res s => - let (ef', args') := builtin_strength_reduction ef args (approx_regs app args) in + let (ef', args') := builtin_strength_reduction app ef args in Ibuiltin ef' args' res s | Icond cond args s1 s2 => match eval_static_condition cond (approx_regs app args) with diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index cd757cd..b223e89 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -469,6 +469,70 @@ Proof. unfold successor; intros. apply match_successor_rec. Qed. +Section BUILTIN_STRENGTH_REDUCTION. +Variable app: D.t. +Variable sp: val. +Variable rs: regset. +Hypothesis MATCH: forall r, val_match_approx ge sp (approx_reg app r) rs#r. + +Lemma annot_strength_reduction_correct: + forall targs args targs' args' eargs, + annot_strength_reduction app targs args = (targs', args') -> + eventval_list_match ge eargs (annot_args_typ targs) rs##args -> + exists eargs', + eventval_list_match ge eargs' (annot_args_typ targs') rs##args' + /\ annot_eventvals targs' eargs' = annot_eventvals targs eargs. +Proof. + induction targs; simpl; intros. +- inv H. simpl. exists eargs; auto. +- destruct a. + + destruct args as [ | arg args0]; simpl in H0; inv H0. + destruct (annot_strength_reduction app targs args0) as [targs'' args''] eqn:E. + exploit IHtargs; eauto. intros [eargs'' [A B]]. + assert (DFL: + exists eargs', + eventval_list_match ge eargs' (annot_args_typ (AA_arg ty :: targs'')) rs##(arg :: args'') + /\ annot_eventvals (AA_arg ty :: targs'') eargs' = ev1 :: annot_eventvals targs evl). + { + exists (ev1 :: eargs''); split. + simpl; constructor; auto. simpl. congruence. + } + destruct ty; destruct (approx_reg app arg) as [] eqn:E2; inv H; auto; + exists eargs''; split; auto; simpl; f_equal; auto; + generalize (MATCH arg); rewrite E2; simpl; intros E3; + rewrite E3 in H5; inv H5; auto. + + destruct (annot_strength_reduction app targs args) as [targs'' args''] eqn:E. + inv H. + exploit IHtargs; eauto. intros [eargs'' [A B]]. + exists eargs''; simpl; split; auto. congruence. + + destruct (annot_strength_reduction app targs args) as [targs'' args''] eqn:E. + inv H. + exploit IHtargs; eauto. intros [eargs'' [A B]]. + exists eargs''; simpl; split; auto. congruence. +Qed. + +Lemma builtin_strength_reduction_correct: + forall ef args m t vres m', + external_call ef ge rs##args m t vres m' -> + let (ef', args') := builtin_strength_reduction app ef args in + external_call ef' ge rs##args' m t vres m'. +Proof. + intros until m'. functional induction (builtin_strength_reduction app ef args); intros; auto. ++ generalize (MATCH r1); rewrite e1; simpl; intros E. simpl in H. + unfold symbol_address in E. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite E in H. + rewrite volatile_load_global_charact. exists b; auto. + inv H. ++ generalize (MATCH r1); rewrite e1; simpl; intros E. simpl in H. + unfold symbol_address in E. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite E in H. + rewrite volatile_store_global_charact. exists b; auto. + inv H. ++ inv H. exploit annot_strength_reduction_correct; eauto. + intros [eargs' [A B]]. + rewrite <- B. econstructor; eauto. +Qed. + +End BUILTIN_STRENGTH_REDUCTION. + (** The proof of semantic preservation is a simulation argument based on "option" diagrams of the following form: << @@ -708,15 +772,15 @@ Proof. (* Ibuiltin *) rename pc'0 into pc. Opaque builtin_strength_reduction. - destruct (builtin_strength_reduction ef args (approx_regs (analyze gapp f)#pc args)) as [ef' args'] eqn:?. - generalize (builtin_strength_reduction_correct ge sp (analyze gapp f)!!pc rs - MATCH2 ef args (approx_regs (analyze gapp f) # pc args) _ _ _ _ (refl_equal _) H0). - rewrite Heqp. intros P. + exploit builtin_strength_reduction_correct; eauto. + TransfInstr. + destruct (builtin_strength_reduction (analyze gapp f)#pc ef args) as [ef' args']. + intros P Q. exploit external_call_mem_extends; eauto. instantiate (1 := rs'##args'). apply regs_lessdef_regs; auto. intros [v' [m2' [A [B [C D]]]]]. left; econstructor; econstructor; split. - eapply exec_Ibuiltin. TransfInstr. rewrite Heqp. eauto. + eapply exec_Ibuiltin. eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. eapply match_states_succ; eauto. simpl; auto. diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml new file mode 100644 index 0000000..1ebb51f --- /dev/null +++ b/backend/PrintAnnot.ml @@ -0,0 +1,76 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Printing annotations in asm syntax *) + +open Printf +open Datatypes +open Integers +open Floats +open Camlcoq +open AST +open Memdata +open Asm + +let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" + +type arg_value = + | Reg of preg + | Stack of memory_chunk * Int.int + | Intconst of Int.int + | Floatconst of float + +let print_annot_text print_preg sp_reg_name oc txt args = + let print_fragment = function + | Str.Text s -> + output_string oc s + | Str.Delim "%%" -> + output_char oc '%' + | Str.Delim s -> + let n = int_of_string (String.sub s 1 (String.length s - 1)) in + try + match List.nth args (n-1) with + | Reg r -> + print_preg oc r + | Stack(chunk, ofs) -> + fprintf oc "mem(%s + %ld, %ld)" + sp_reg_name + (camlint_of_coqint ofs) + (camlint_of_coqint (size_chunk chunk)) + | Intconst n -> + fprintf oc "%ld" (camlint_of_coqint n) + | Floatconst n -> + fprintf oc "%.18g" (camlfloat_of_coqfloat n) + with Failure _ -> + fprintf oc "" s in + List.iter print_fragment (Str.full_split re_annot_param txt); + fprintf oc "\n" + +let rec annot_args tmpl args = + match tmpl, args with + | [], _ -> [] + | AA_arg _ :: tmpl', APreg r :: args' -> + Reg r :: annot_args tmpl' args' + | AA_arg _ :: tmpl', APstack(chunk, ofs) :: args' -> + Stack(chunk, ofs) :: annot_args tmpl' args' + | AA_arg _ :: tmpl', [] -> [] (* should never happen *) + | AA_int n :: tmpl', _ -> + Intconst n :: annot_args tmpl' args + | AA_float n :: tmpl', _ -> + Floatconst n :: annot_args tmpl' args + +let print_annot_stmt print_preg sp_reg_name oc txt tmpl args = + print_annot_text print_preg sp_reg_name oc txt (annot_args tmpl args) + +let print_annot_val print_preg oc txt args = + print_annot_text print_preg "" oc txt + (List.map (fun r -> Reg r) args) -- cgit v1.2.3