Constant propagation within __builtin_annot.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 185 insertions, 7 deletions

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 "<bad parameter %s>" 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 "<internal error>" oc txt
+    (List.map (fun r -> Reg r) args)