Merge of the newmem branch:

- Revised memory model with Max and Cur permissions, but without bounds
- Constant propagation of 'const' globals
- Function inlining at RTL level
- (Unprovable) elimination of unreferenced static definitions


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

1 files changed, 410 insertions, 86 deletions

diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 9affea88..406e6133 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -31,11 +31,18 @@ Require Import ConstpropOp.
 Require Import Constprop.
 Require Import ConstpropOpproof.
 
+Section PRESERVATION.
+
+Variable prog: program.
+Let tprog := transf_program prog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+Let gapp := make_global_approx (PTree.empty _) prog.(prog_vars).
+
 (** * Correctness of the static analysis *)
 
 Section ANALYSIS.
 
-Variable ge: genv.
 Variable sp: val.
 
 Definition regs_match_approx (a: D.t) (rs: regset) : Prop :=
@@ -97,14 +104,14 @@ Lemma analyze_correct_1:
   forall f pc rs pc' i,
   f.(fn_code)!pc = Some i ->
   In pc' (successors_instr i) ->
-  regs_match_approx (transfer f pc (analyze f)!!pc) rs ->
-  regs_match_approx (analyze f)!!pc' rs.
+  regs_match_approx (transfer gapp f pc (analyze gapp f)!!pc) rs ->
+  regs_match_approx (analyze gapp f)!!pc' rs.
 Proof.
   intros until i. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (transfer f)
+  caseEq (DS.fixpoint (successors f) (transfer gapp f)
                       ((fn_entrypoint f, D.top) :: nil)).
   intros approxs; intros.
-  apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
+  apply regs_match_approx_increasing with (transfer gapp f pc approxs!!pc).
   eapply DS.fixpoint_solution; eauto.
   unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto.
   auto.
@@ -113,10 +120,10 @@ Qed.
 
 Lemma analyze_correct_3:
   forall f rs,
-  regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs.
+  regs_match_approx (analyze gapp f)!!(f.(fn_entrypoint)) rs.
 Proof.
   intros. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (transfer f)
+  caseEq (DS.fixpoint (successors f) (transfer gapp f)
                       ((fn_entrypoint f, D.top) :: nil)).
   intros approxs; intros.
   apply regs_match_approx_increasing with D.top.
@@ -125,6 +132,301 @@ Proof.
   intros. rewrite PMap.gi. apply regs_match_approx_top.
 Qed.
 
+(** eval_static_load *)
+
+Definition mem_match_approx (m: mem) : Prop :=
+  forall id il b,
+  gapp!id = Some il -> Genv.find_symbol ge id = Some b ->
+  Genv.load_store_init_data ge m b 0 il /\
+  Mem.valid_block m b /\
+  (forall ofs, ~Mem.perm m b ofs Max Writable).
+
+Lemma eval_load_init_sound:
+  forall chunk m b il base ofs pos v,
+  Genv.load_store_init_data ge m b base il ->
+  Mem.load chunk m b ofs = Some v ->
+  ofs = base + pos ->
+  val_match_approx ge sp (eval_load_init chunk pos il) v.
+Proof.
+  induction il; simpl; intros.
+(* base case il = nil *)
+  auto.
+(* inductive case *)
+  destruct a.
+  (* Init_int8 *)
+  destruct H. destruct (zeq pos 0). subst.  rewrite Zplus_0_r in H0.
+  destruct chunk; simpl; auto.
+  rewrite Mem.load_int8_signed_unsigned in H0. rewrite H in H0. simpl in H0.
+  inv H0. decEq. apply Int.sign_ext_zero_ext. compute; auto. 
+  congruence.
+  eapply IHil; eauto. omega.
+  (* Init_int16 *)
+  destruct H. destruct (zeq pos 0). subst.  rewrite Zplus_0_r in H0.
+  destruct chunk; simpl; auto.
+  rewrite Mem.load_int16_signed_unsigned in H0. rewrite H in H0. simpl in H0.
+  inv H0. decEq. apply Int.sign_ext_zero_ext. compute; auto. 
+  congruence.
+  eapply IHil; eauto. omega.
+  (* Init_int32 *)
+  destruct H. destruct (zeq pos 0). subst.  rewrite Zplus_0_r in H0.
+  destruct chunk; simpl; auto.
+  congruence.
+  eapply IHil; eauto. omega.
+  (* Init_float32 *)
+  destruct H. destruct (zeq pos 0). subst.  rewrite Zplus_0_r in H0.
+  destruct chunk; simpl; auto. destruct (propagate_float_constants tt); simpl; auto.
+  congruence.
+  eapply IHil; eauto. omega.
+  (* Init_float64 *)
+  destruct H. destruct (zeq pos 0). subst.  rewrite Zplus_0_r in H0.
+  destruct chunk; simpl; auto. destruct (propagate_float_constants tt); simpl; auto.
+  congruence.
+  eapply IHil; eauto. omega.
+  (* Init_space *)
+  eapply IHil; eauto. omega.
+  (* Init_symbol *)
+  destruct H as [[b' [A B]] C].
+  destruct (zeq pos 0). subst.  rewrite Zplus_0_r in H0.
+  destruct chunk; simpl; auto.
+  unfold symbol_address. rewrite A. congruence.
+  eapply IHil; eauto. omega.
+Qed.
+
+Lemma eval_static_load_sound:
+  forall chunk m addr vaddr v,
+  Mem.loadv chunk m vaddr = Some v ->
+  mem_match_approx m ->  
+  val_match_approx ge sp addr vaddr ->
+  val_match_approx ge sp (eval_static_load gapp chunk addr) v.
+Proof.
+  intros. unfold eval_static_load. destruct addr; simpl; auto. 
+  destruct (gapp!i) as [il|]_eqn; auto.
+  red in H1. subst vaddr. unfold symbol_address in H. 
+  destruct (Genv.find_symbol ge i) as [b'|]_eqn; simpl in H; try discriminate.
+  exploit H0; eauto. intros [A [B C]]. 
+  eapply eval_load_init_sound; eauto. 
+  red; auto. 
+Qed.
+
+Lemma mem_match_approx_store:
+  forall chunk m addr v m',
+  mem_match_approx m ->
+  Mem.storev chunk m addr v = Some m' ->
+  mem_match_approx m'.
+Proof.
+  intros; red; intros. exploit H; eauto. intros [A [B C]].
+  destruct addr; simpl in H0; try discriminate.
+  exploit Mem.store_valid_access_3; eauto. intros [P Q].
+  split. apply Genv.load_store_init_data_invariant with m; auto. 
+  intros. eapply Mem.load_store_other; eauto. left; red; intro; subst b0.
+  eapply C. apply Mem.perm_cur_max. eapply P. instantiate (1 := Int.unsigned i).
+  generalize (size_chunk_pos chunk). omega.
+  split. eauto with mem.
+  intros; red; intros. eapply C. eapply Mem.perm_store_2; eauto.
+Qed.
+
+Lemma mem_match_approx_alloc:
+  forall m lo hi b m',
+  mem_match_approx m ->
+  Mem.alloc m lo hi = (m', b) ->
+  mem_match_approx m'.
+Proof.
+  intros; red; intros. exploit H; eauto. intros [A [B C]].
+  split. apply Genv.load_store_init_data_invariant with m; auto.
+  intros. eapply Mem.load_alloc_unchanged; eauto. 
+  split. eauto with mem.
+  intros; red; intros. exploit Mem.perm_alloc_inv; eauto. 
+  rewrite zeq_false. apply C. eapply Mem.valid_not_valid_diff; eauto with mem.
+Qed.
+
+Lemma mem_match_approx_free:
+  forall m lo hi b m',
+  mem_match_approx m ->
+  Mem.free m b lo hi = Some m' ->
+  mem_match_approx m'.
+Proof.
+  intros; red; intros. exploit H; eauto. intros [A [B C]].
+  split. apply Genv.load_store_init_data_invariant with m; auto.
+  intros. eapply Mem.load_free; eauto.
+  destruct (zeq b0 b); auto. subst b0.
+  right. destruct (zlt lo hi); auto. 
+  elim (C lo). apply Mem.perm_cur_max. 
+  exploit Mem.free_range_perm; eauto. instantiate (1 := lo); omega. 
+  intros; eapply Mem.perm_implies; eauto with mem.
+  split. eauto with mem.
+  intros; red; intros. eapply C. eauto with mem. 
+Qed.
+
+Lemma mem_match_approx_extcall:
+  forall ef vargs m t vres m',
+  mem_match_approx m ->
+  external_call ef ge vargs m t vres m' ->
+  mem_match_approx m'.
+Proof.
+  intros; red; intros. exploit H; eauto. intros [A [B C]].
+  split. apply Genv.load_store_init_data_invariant with m; auto.
+  intros. eapply external_call_readonly; eauto. 
+  split. eapply external_call_valid_block; eauto.
+  intros; red; intros. elim (C ofs). eapply external_call_max_perm; eauto. 
+Qed.
+
+(* Show that mem_match_approx holds initially *)
+
+Definition global_approx_charact (g: genv) (ga: global_approx) : Prop :=
+  forall id il b,
+  ga!id = Some il -> 
+  Genv.find_symbol g id = Some b -> 
+  Genv.find_var_info g b = Some (mkglobvar tt il true false).
+
+Lemma make_global_approx_correct:
+  forall vl g ga,
+  global_approx_charact g ga ->
+  global_approx_charact (Genv.add_variables g vl) (make_global_approx ga vl).
+Proof.
+  induction vl; simpl; intros.
+  auto.
+  destruct a as [id gv]. apply IHvl. 
+  red; intros. 
+  assert (EITHER: id0 = id /\ gv = mkglobvar tt il true false
+               \/ id0 <> id /\ ga!id0 = Some il).
+  destruct (gvar_readonly gv && negb (gvar_volatile gv)) as []_eqn.
+  rewrite PTree.gsspec in H0. destruct (peq id0 id).
+  inv H0. left. split; auto. 
+  destruct gv; simpl in *. 
+  destruct gvar_readonly; try discriminate.
+  destruct gvar_volatile; try discriminate.
+  destruct gvar_info. auto.
+  right; auto.
+  rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); try discriminate.
+  right; auto.
+  unfold Genv.add_variable, Genv.find_symbol, Genv.find_var_info in *;
+  simpl in *.
+  destruct EITHER as [[A B] | [A B]].
+  subst id0. rewrite PTree.gss in H1. inv H1. rewrite ZMap.gss. auto.
+  rewrite PTree.gso in H1; auto. rewrite ZMap.gso. eapply H. eauto. auto.
+  exploit Genv.genv_symb_range; eauto. unfold ZIndexed.t. omega.
+Qed.
+
+Theorem mem_match_approx_init:
+  forall m, Genv.init_mem prog = Some m -> mem_match_approx m.
+Proof.
+  intros. 
+  assert (global_approx_charact ge gapp).
+    unfold ge, gapp.   unfold Genv.globalenv.
+    apply make_global_approx_correct.
+    red; intros. rewrite PTree.gempty in H0; discriminate.
+  red; intros. 
+  exploit Genv.init_mem_characterization.
+  unfold ge in H0. eapply H0; eauto. eauto. 
+  unfold Genv.perm_globvar; simpl.
+  intros [A [B C]].
+  split. auto. split. eapply Genv.find_symbol_not_fresh; eauto. 
+  intros; red; intros. exploit B; eauto. intros [P Q]. inv Q.
+Qed.
+
+(**********************
+Definition mem_match_approx_gen (g: genv) (ga: global_approx) (m: mem) : Prop :=
+  forall id il b,
+  ga!id = Some il -> Genv.find_symbol g id = Some b ->
+  Genv.load_store_init_data ge m b 0 il /\
+  Mem.valid_block m b /\
+  (forall ofs, ~Mem.perm m b ofs Max Writable).
+
+Lemma mem_match_approx_alloc_variables:
+  forall vl g ga m m',
+  mem_match_approx_gen g ga m ->
+  Genv.genv_nextvar g = Mem.nextblock m ->
+  Genv.alloc_variables ge m vl = Some m' ->
+  mem_match_approx_gen (Genv.add_variables g vl) (make_global_approx ga vl) m'.
+Proof.
+  induction vl; simpl; intros.
+(* base case *)
+  inv H1. auto.
+(* inductive case *)
+  destruct a as [id gv].
+  set (ga1 := if gv.(gvar_readonly) && negb gv.(gvar_volatile)
+        then PTree.set id gv.(gvar_init) ga
+        else PTree.remove id ga).
+  revert H1. unfold Genv.alloc_variable. simpl.
+  set (il := gvar_init gv) in *.
+  set (sz := Genv.init_data_list_size il) in *.
+  destruct (Mem.alloc m 0 sz) as [m1 b]_eqn.
+  destruct (Genv.store_zeros m1 b sz) as [m2|]_eqn; try congruence.
+  destruct (Genv.store_init_data_list ge m2 b 0 il) as [m3|]_eqn; try congruence.
+  destruct (Mem.drop_perm m3 b 0 sz (Genv.perm_globvar gv)) as [m4|]_eqn; try congruence.
+  intros. 
+  exploit Mem.alloc_result; eauto. intro NB. 
+  assert (NB': Mem.nextblock m4 = Mem.nextblock m1).
+  rewrite (Mem.nextblock_drop _ _ _ _ _ _ Heqo1).
+  rewrite (Genv.store_init_data_list_nextblock _ _ _ _ _ Heqo0).
+  rewrite (Genv.store_zeros_nextblock _ _ _ Heqo). 
+  auto.
+  apply IHvl with m4. 
+  (* mem_match_approx for intermediate state *)
+  red; intros.
+  unfold Genv.find_symbol in H3. simpl in H3. 
+  rewrite H0 in H3. rewrite <- NB in H3. 
+  assert (EITHER: id0 <> id /\ ga!id0 = Some il0
+       \/ id0 = id /\ il0 = il /\ gvar_readonly gv = true /\ gvar_volatile gv = false).
+  unfold ga1 in H2. destruct (gvar_readonly gv && negb (gvar_volatile gv)) as []_eqn. 
+  rewrite PTree.gsspec in H2. destruct (peq id0 id).
+  inv H2. right. split; auto. split; auto. 
+  destruct (gvar_readonly gv); simpl in Heqb1; try discriminate.
+  destruct (gvar_volatile gv); simpl in Heqb1; try discriminate.
+  auto. auto.
+  rewrite PTree.grspec in H2. destruct (PTree.elt_eq id0 id); try discriminate.
+  auto.   
+  destruct EITHER as [[A B] | [A [B [C D]]]].
+  (* older blocks *)
+  rewrite PTree.gso in H3; auto. exploit H; eauto. intros [P [Q R]].
+  assert (b0 <> b). eapply Mem.valid_not_valid_diff; eauto with mem.
+  split. apply Genv.load_store_init_data_invariant with m; auto. 
+  intros. transitivity (Mem.load chunk m3 b0 ofs). eapply Mem.load_drop; eauto.
+  transitivity (Mem.load chunk m2 b0 ofs). eapply Genv.store_init_data_list_outside; eauto.
+  transitivity (Mem.load chunk m1 b0 ofs). eapply Genv.store_zeros_outside; eauto.
+  eapply Mem.load_alloc_unchanged; eauto.  
+  split. red. rewrite NB'.  change (Mem.valid_block m1 b0). eauto with mem.
+  intros; red; intros. elim (R ofs). 
+  eapply Mem.perm_alloc_4; eauto.
+  rewrite Genv.store_zeros_perm; [idtac|eauto].
+  rewrite Genv.store_init_data_list_perm; [idtac|eauto].
+  eapply Mem.perm_drop_4; eauto.
+  (* same block *)
+  subst id0 il0. rewrite PTree.gss in H3. injection H3; intro EQ; subst b0.
+  unfold Genv.perm_globvar in Heqo1.
+  rewrite D in Heqo1. rewrite C in Heqo1.
+  split. apply Genv.load_store_init_data_invariant with m3.
+  intros. eapply Mem.load_drop; eauto. do 3 right. auto with mem. 
+  eapply Genv.store_init_data_list_charact; eauto. 
+  split. red. rewrite NB'. change (Mem.valid_block m1 b). eauto with mem.
+  intros; red; intros. 
+  assert (0 <= ofs < sz).
+    eapply Mem.perm_alloc_3; eauto.
+    rewrite Genv.store_zeros_perm; [idtac|eauto].
+    rewrite Genv.store_init_data_list_perm; [idtac|eauto].
+    eapply Mem.perm_drop_4; eauto.
+  assert (PO: perm_order Readable Writable).
+    eapply Mem.perm_drop_2; eauto. 
+  inv PO. 
+  (* nextvar hyp *)
+  simpl. rewrite NB'. rewrite (Mem.nextblock_alloc _ _ _ _ _ Heqp).
+  unfold block in *; omega.
+  (* alloc vars hyp *)
+  auto.
+Qed.
+
+Theorem mem_match_approx_init:
+  forall m, Genv.init_mem prog = Some m -> mem_match_approx m.
+Proof.
+  intros. unfold Genv.init_mem in H. 
+  eapply mem_match_approx_alloc_variables; eauto.
+(* mem_match_approx on empty list *)
+  red; intros. rewrite PTree.gempty in H0. discriminate.
+(* nextvar *)
+  rewrite Genv.add_functions_nextvar. auto.
+Qed.
+********************************)
+
 End ANALYSIS.
 
 (** * Correctness of the code transformation *)
@@ -132,13 +434,6 @@ End ANALYSIS.
 (** We now show that the transformed code after constant propagation
   has the same semantics as the original code. *)
 
-Section PRESERVATION.
-
-Variable prog: program.
-Let tprog := transf_program prog.
-Let ge := Genv.globalenv prog.
-Let tge := Genv.globalenv tprog.
-
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
 Proof.
@@ -156,24 +451,24 @@ Qed.
 Lemma functions_translated:
   forall (v: val) (f: fundef),
   Genv.find_funct ge v = Some f ->
-  Genv.find_funct tge v = Some (transf_fundef f).
+  Genv.find_funct tge v = Some (transf_fundef gapp f).
 Proof.  
   intros.
-  exact (Genv.find_funct_transf transf_fundef _ _ H).
+  exact (Genv.find_funct_transf (transf_fundef gapp) _ _ H).
 Qed.
 
 Lemma function_ptr_translated:
   forall (b: block) (f: fundef),
   Genv.find_funct_ptr ge b = Some f ->
-  Genv.find_funct_ptr tge b = Some (transf_fundef f).
+  Genv.find_funct_ptr tge b = Some (transf_fundef gapp f).
 Proof.  
   intros. 
-  exact (Genv.find_funct_ptr_transf transf_fundef _ _ H).
+  exact (Genv.find_funct_ptr_transf (transf_fundef gapp) _ _ H).
 Qed.
 
 Lemma sig_function_translated:
   forall f,
-  funsig (transf_fundef f) = funsig f.
+  funsig (transf_fundef gapp f) = funsig f.
 Proof.
   intros. destruct f; reflexivity.
 Qed.
@@ -209,17 +504,17 @@ Qed.
 
 Lemma transf_ros_correct:
   forall sp ros rs rs' f approx,
-  regs_match_approx ge sp approx rs ->
+  regs_match_approx sp approx rs ->
   find_function ge ros rs = Some f ->
   regs_lessdef rs rs' ->
-  find_function tge (transf_ros approx ros) rs' = Some (transf_fundef f).
+  find_function tge (transf_ros approx ros) rs' = Some (transf_fundef gapp f).
 Proof.
   intros. destruct ros; simpl in *.
   generalize (H r); intro MATCH. generalize (H1 r); intro LD.
   destruct (rs#r); simpl in H0; try discriminate.
   destruct (Int.eq_dec i Int.zero); try discriminate.
   inv LD. 
-  assert (find_function tge (inl _ r) rs' = Some (transf_fundef f)).
+  assert (find_function tge (inl _ r) rs' = Some (transf_fundef gapp f)).
     simpl. rewrite <- H4. simpl. rewrite dec_eq_true. apply function_ptr_translated. auto.
   destruct (D.get r approx); auto.
   predSpec Int.eq Int.eq_spec i0 Int.zero; intros; auto.
@@ -230,6 +525,20 @@ Proof.
   apply function_ptr_translated; auto.
 Qed.
 
+Lemma const_for_result_correct:
+  forall a op sp v m,
+  const_for_result a = Some op ->
+  val_match_approx ge sp a v ->
+  eval_operation tge sp op nil m = Some v.
+Proof.
+  unfold const_for_result; intros. 
+  destruct a; inv H; simpl in H0.
+  simpl. congruence.
+  destruct (generate_float_constants tt); inv H2.  simpl. congruence.
+  simpl. subst v. unfold symbol_address. rewrite symbols_preserved. auto.
+  simpl. congruence.
+Qed.
+
 (** The proof of semantic preservation is a simulation argument
   based on diagrams of the following form:
 <<
@@ -259,29 +568,32 @@ Inductive match_stackframes: stackframe -> stackframe -> Prop :=
    match_stackframe_intro:
       forall res sp pc rs f rs',
       regs_lessdef rs rs' ->
-      (forall v, regs_match_approx ge sp (analyze f)!!pc (rs#res <- v)) ->
+      (forall v, regs_match_approx sp (analyze gapp f)!!pc (rs#res <- v)) ->
     match_stackframes
         (Stackframe res f sp pc rs)
-        (Stackframe res (transf_function f) sp pc rs').
+        (Stackframe res (transf_function gapp f) sp pc rs').
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
       forall s sp pc rs m f s' rs' m'
-           (MATCH: regs_match_approx ge sp (analyze f)!!pc rs)
+           (MATCH: regs_match_approx sp (analyze gapp f)!!pc rs)
+           (GMATCH: mem_match_approx m)
            (STACKS: list_forall2 match_stackframes s s')
            (REGS: regs_lessdef rs rs')
            (MEM: Mem.extends m m'),
       match_states (State s f sp pc rs m)
-                   (State s' (transf_function f) sp pc rs' m')
+                   (State s' (transf_function gapp f) sp pc rs' m')
   | match_states_call:
       forall s f args m s' args' m'
+           (GMATCH: mem_match_approx m)
            (STACKS: list_forall2 match_stackframes s s')
            (ARGS: Val.lessdef_list args args')
            (MEM: Mem.extends m m'),
       match_states (Callstate s f args m)
-                   (Callstate s' (transf_fundef f) args' m')
+                   (Callstate s' (transf_fundef gapp f) args' m')
   | match_states_return:
       forall s v m s' v' m'
+           (GMATCH: mem_match_approx m)
            (STACKS: list_forall2 match_stackframes s s')
            (RES: Val.lessdef v v')
            (MEM: Mem.extends m m'),
@@ -292,7 +604,7 @@ Inductive match_states: state -> state -> Prop :=
 Ltac TransfInstr :=
   match goal with
   | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ =>
-      cut ((transf_function f).(fn_code)!pc = Some(transf_instr (analyze f)!!pc instr));
+      cut ((transf_function gapp f).(fn_code)!pc = Some(transf_instr gapp (analyze gapp f)!!pc instr));
       [ simpl transf_instr
       | unfold transf_function, transf_code; simpl; rewrite PTree.gmap; 
         unfold option_map; rewrite H1; reflexivity ]
@@ -310,7 +622,7 @@ Proof.
   induction 1; intros; inv MS.
 
   (* Inop *)
-  exists (State s' (transf_function f) sp pc' rs' m'); split.
+  exists (State s' (transf_function gapp f) sp pc' rs' m'); split.
   TransfInstr; intro. eapply exec_Inop; eauto.
   econstructor; eauto.
   eapply analyze_correct_1 with (pc := pc); eauto.
@@ -318,70 +630,73 @@ Proof.
   unfold transfer; rewrite H. auto.
 
   (* Iop *)
-  assert (MATCH': regs_match_approx ge sp (analyze f) # pc' rs # res <- v).
+  TransfInstr.
+  set (a := eval_static_operation op (approx_regs (analyze gapp f)#pc args)).
+  assert (VMATCH: val_match_approx ge sp a v).  
+    eapply eval_static_operation_correct; eauto.
+    apply approx_regs_val_list; auto.
+  assert (MATCH': regs_match_approx sp (analyze gapp f) # pc' rs # res <- v).
     eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto.
     unfold transfer; rewrite H. 
     apply regs_match_approx_update; auto. 
-    eapply eval_static_operation_correct; eauto.
-    apply approx_regs_val_list; auto.
-  TransfInstr.
-  exploit eval_static_operation_correct; eauto. eapply approx_regs_val_list; eauto. intros VM.
-  destruct (eval_static_operation op (approx_regs (analyze f) # pc args)); intros; simpl in VM.
-  (* Novalue *)
-  contradiction.
-  (* Unknown *)
+  destruct (const_for_result a) as [cop|]_eqn; intros.
+  (* constant is propagated *)
+  exists (State s' (transf_function gapp f) sp pc' (rs'#res <- v) m'); split.
+  eapply exec_Iop; eauto. 
+  eapply const_for_result_correct; eauto.
+  econstructor; eauto. 
+  apply set_reg_lessdef; auto.
+  (* operator is strength-reduced *)
   exploit op_strength_reduction_correct. eexact MATCH. reflexivity. eauto. 
-  destruct (op_strength_reduction op args (approx_regs (analyze f) # pc args)) as [op' args'].
+  destruct (op_strength_reduction op args (approx_regs (analyze gapp f) # pc args)) as [op' args'].
   intros [v' [EV' LD']].
   assert (EV'': exists v'', eval_operation ge sp op' rs'##args' m' = Some v'' /\ Val.lessdef v' v'').
-    eapply eval_operation_lessdef; eauto. eapply regs_lessdef_regs; eauto.
+  eapply eval_operation_lessdef; eauto. eapply regs_lessdef_regs; eauto.
   destruct EV'' as [v'' [EV'' LD'']].
-  exists (State s' (transf_function f) sp pc' (rs'#res <- v'') m'); split.
+  exists (State s' (transf_function gapp f) sp pc' (rs'#res <- v'') m'); split.
   econstructor. eauto. rewrite <- EV''. apply eval_operation_preserved. exact symbols_preserved.
   econstructor; eauto. apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto.
-  (* I i *)
-  subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Vint i)) m'); split.
-  econstructor; eauto.
-  econstructor; eauto. apply set_reg_lessdef; auto.
-  (* F *)
-  subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Vfloat f0)) m'); split.
-  econstructor; eauto.
-  econstructor; eauto. apply set_reg_lessdef; auto.
-  (* G *)
-  subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (symbol_address tge i i0)) m'); split.
-  econstructor; eauto.
-  econstructor; eauto. apply set_reg_lessdef; auto.
-  unfold symbol_address. rewrite symbols_preserved; auto. 
-  (* S *)
-  subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Val.add sp (Vint i))) m'); split.
-  econstructor; eauto.
-  econstructor; eauto. apply set_reg_lessdef; auto.
 
   (* Iload *)
   TransfInstr. 
-  generalize (addr_strength_reduction_correct ge sp (analyze f)!!pc rs
-                  MATCH addr args (approx_regs (analyze f) # pc args) (refl_equal _)).
-  destruct (addr_strength_reduction addr args (approx_regs (analyze f) # pc args)) as [addr' args'].
-  intros P Q. rewrite H0 in P.
+  set (ap1 := eval_static_addressing addr
+               (approx_regs (analyze gapp f) # pc args)).
+  set (ap2 := eval_static_load gapp chunk ap1).
+  assert (VM1: val_match_approx ge sp ap1 a).
+    eapply eval_static_addressing_correct; eauto.
+    eapply approx_regs_val_list; eauto.
+  assert (VM2: val_match_approx ge sp ap2 v).
+    eapply eval_static_load_sound; eauto.
+  assert (MATCH': regs_match_approx sp (analyze gapp f) # pc' rs # dst <- v).
+    eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto.
+    unfold transfer; rewrite H. 
+    apply regs_match_approx_update; auto. 
+  destruct (const_for_result ap2) as [cop|]_eqn; intros.
+  (* constant-propagated *)
+  exists (State s' (transf_function gapp f) sp pc' (rs'#dst <- v) m'); split.
+  eapply exec_Iop; eauto. eapply const_for_result_correct; eauto.
+  econstructor; eauto. apply set_reg_lessdef; auto.
+  (* strength-reduced *)
+  generalize (addr_strength_reduction_correct ge sp (analyze gapp f)!!pc rs
+                  MATCH addr args (approx_regs (analyze gapp f) # pc args) (refl_equal _)).
+  destruct (addr_strength_reduction addr args (approx_regs (analyze gapp f) # pc args)) as [addr' args'].
+  rewrite H0. intros P.
   assert (ADDR': exists a', eval_addressing ge sp addr' rs'##args' = Some a' /\ Val.lessdef a a').
     eapply eval_addressing_lessdef; eauto. eapply regs_lessdef_regs; eauto.
   destruct ADDR' as [a' [A B]].
   assert (C: eval_addressing tge sp addr' rs'##args' = Some a').
     rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
   exploit Mem.loadv_extends; eauto. intros [v' [D E]].
-  exists (State s' (transf_function f) sp pc' (rs'#dst <- v') m'); split.
+  exists (State s' (transf_function gapp f) sp pc' (rs'#dst <- v') m'); split.
   eapply exec_Iload; eauto.
   econstructor; eauto. 
-  eapply analyze_correct_1; eauto. simpl; auto. 
-  unfold transfer; rewrite H. 
-  apply regs_match_approx_update; auto. simpl; auto.
   apply set_reg_lessdef; auto. 
 
   (* Istore *)
   TransfInstr.
-  generalize (addr_strength_reduction_correct ge sp (analyze f)!!pc rs
-                  MATCH addr args (approx_regs (analyze f) # pc args) (refl_equal _)).
-  destruct (addr_strength_reduction addr args (approx_regs (analyze f) # pc args)) as [addr' args'].
+  generalize (addr_strength_reduction_correct ge sp (analyze gapp f)!!pc rs
+                  MATCH addr args (approx_regs (analyze gapp f) # pc args) (refl_equal _)).
+  destruct (addr_strength_reduction addr args (approx_regs (analyze gapp f) # pc args)) as [addr' args'].
   intros P Q. rewrite H0 in P.
   assert (ADDR': exists a', eval_addressing ge sp addr' rs'##args' = Some a' /\ Val.lessdef a a').
     eapply eval_addressing_lessdef; eauto. eapply regs_lessdef_regs; eauto.
@@ -389,11 +704,12 @@ Proof.
   assert (C: eval_addressing tge sp addr' rs'##args' = Some a').
     rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
   exploit Mem.storev_extends; eauto. intros [m2' [D E]].
-  exists (State s' (transf_function f) sp pc' rs' m2'); split.
+  exists (State s' (transf_function gapp f) sp pc' rs' m2'); split.
   eapply exec_Istore; eauto.
   econstructor; eauto. 
   eapply analyze_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. auto. 
+  eapply mem_match_approx_store; eauto.
 
   (* Icall *)
   exploit transf_ros_correct; eauto. intro FIND'.
@@ -413,18 +729,20 @@ Proof.
   TransfInstr; intro.
   econstructor; split.
   eapply exec_Itailcall; eauto. apply sig_function_translated; auto.
-  constructor; auto. apply regs_lessdef_regs; auto. 
+  constructor; auto. 
+  eapply mem_match_approx_free; eauto.
+  apply regs_lessdef_regs; auto. 
 
   (* Ibuiltin *)
 Opaque builtin_strength_reduction.
-  destruct (builtin_strength_reduction ef args (approx_regs (analyze f)#pc args)) as [ef' args']_eqn.
-  generalize (builtin_strength_reduction_correct ge sp (analyze f)!!pc rs
-                  MATCH ef args (approx_regs (analyze f) # pc args) _ _ _ _ (refl_equal _) H0).
+  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
+                  MATCH ef args (approx_regs (analyze gapp f) # pc args) _ _ _ _ (refl_equal _) H0).
   rewrite Heqp. intros P.
   exploit external_call_mem_extends; eauto. 
   instantiate (1 := rs'##args'). apply regs_lessdef_regs; auto.
   intros [v' [m2' [A [B [C D]]]]].
-  exists (State s' (transf_function f) sp pc' (rs'#res <- v') m2'); split.
+  exists (State s' (transf_function gapp f) sp pc' (rs'#res <- v') m2'); split.
   eapply exec_Ibuiltin. TransfInstr. rewrite Heqp. eauto.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
@@ -432,16 +750,17 @@ Opaque builtin_strength_reduction.
   eapply analyze_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. 
   apply regs_match_approx_update; auto. simpl; auto.
+  eapply mem_match_approx_extcall; eauto. 
   apply set_reg_lessdef; auto.
 
   (* Icond *)
   TransfInstr. 
-  generalize (cond_strength_reduction_correct ge sp (analyze f)#pc rs m
-                    MATCH cond args (approx_regs (analyze f) # pc args) (refl_equal _)).
-  destruct (cond_strength_reduction cond args (approx_regs (analyze f) # pc args)) as [cond' args'].
+  generalize (cond_strength_reduction_correct ge sp (analyze gapp f)#pc rs m
+                    MATCH cond args (approx_regs (analyze gapp f) # pc args) (refl_equal _)).
+  destruct (cond_strength_reduction cond args (approx_regs (analyze gapp f) # pc args)) as [cond' args'].
   intros EV1. 
-  exists (State s' (transf_function f) sp (if b then ifso else ifnot) rs' m'); split. 
-  destruct (eval_static_condition cond (approx_regs (analyze f) # pc args)) as []_eqn.
+  exists (State s' (transf_function gapp f) sp (if b then ifso else ifnot) rs' m'); split. 
+  destruct (eval_static_condition cond (approx_regs (analyze gapp f) # pc args)) as []_eqn.
   assert (eval_condition cond rs ## args m = Some b0).
     eapply eval_static_condition_correct; eauto. eapply approx_regs_val_list; eauto.
   assert (b = b0) by congruence. subst b0.
@@ -453,14 +772,14 @@ Opaque builtin_strength_reduction.
   unfold transfer; rewrite H. auto. 
 
   (* Ijumptable *)
-  assert (A: (fn_code (transf_function f))!pc = Some(Ijumptable arg tbl)
-             \/ (fn_code (transf_function f))!pc = Some(Inop pc')).
-  TransfInstr. destruct (approx_reg (analyze f) # pc arg) as []_eqn; auto.
+  assert (A: (fn_code (transf_function gapp f))!pc = Some(Ijumptable arg tbl)
+             \/ (fn_code (transf_function gapp f))!pc = Some(Inop pc')).
+  TransfInstr. destruct (approx_reg (analyze gapp f) # pc arg) as []_eqn; auto.
   generalize (MATCH arg). unfold approx_reg in Heqt. rewrite Heqt. rewrite H0. 
   simpl. intro EQ; inv EQ. rewrite H1. auto.
   assert (B: rs'#arg = Vint n).
   generalize (REGS arg); intro LD; inv LD; congruence.
-  exists (State s' (transf_function f) sp pc' rs' m'); split.
+  exists (State s' (transf_function gapp f) sp pc' rs' m'); split.
   destruct A. eapply exec_Ijumptable; eauto. eapply exec_Inop; eauto. 
   econstructor; eauto.
   eapply analyze_correct_1; eauto.
@@ -472,6 +791,7 @@ Opaque builtin_strength_reduction.
   exists (Returnstate s' (regmap_optget or Vundef rs') m2'); split.
   eapply exec_Ireturn; eauto. TransfInstr; auto.
   constructor; auto.
+  eapply mem_match_approx_free; eauto.
   destruct or; simpl; auto. 
 
   (* internal function *)
@@ -482,6 +802,7 @@ Opaque builtin_strength_reduction.
   eapply exec_function_internal; simpl; eauto.
   simpl. econstructor; eauto.
   apply analyze_correct_3; auto.
+  eapply mem_match_approx_alloc; eauto.
   apply init_regs_lessdef; auto.
 
   (* external function *)
@@ -492,6 +813,7 @@ Opaque builtin_strength_reduction.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   constructor; auto.
+  eapply mem_match_approx_extcall; eauto.
 
   (* return *)
   inv H3. inv H1. 
@@ -506,14 +828,16 @@ Lemma transf_initial_states:
 Proof.
   intros. inversion H.
   exploit function_ptr_translated; eauto. intro FIND.
-  exists (Callstate nil (transf_fundef f) nil m0); split.
+  exists (Callstate nil (transf_fundef gapp f) nil m0); split.
   econstructor; eauto.
   apply Genv.init_mem_transf; auto.
   replace (prog_main tprog) with (prog_main prog).
   rewrite symbols_preserved. eauto.
   reflexivity.
   rewrite <- H3. apply sig_function_translated.
-  constructor. constructor. constructor. apply Mem.extends_refl.
+  constructor. 
+  eapply mem_match_approx_init; eauto.
+  constructor. constructor. apply Mem.extends_refl.
 Qed.
 
 Lemma transf_final_states: