diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Inliningproof.v | 30 | ||||
-rw-r--r-- | backend/NeedDomain.v | 4 | ||||
-rw-r--r-- | backend/Stackingproof.v | 50 | ||||
-rw-r--r-- | backend/Unusedglobproof.v | 34 | ||||
-rw-r--r-- | backend/ValueAnalysis.v | 2 | ||||
-rw-r--r-- | backend/ValueDomain.v | 6 |
6 files changed, 63 insertions, 63 deletions
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index e3c5bf2a..993e0b34 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -109,11 +109,11 @@ Qed. (** ** Agreement between register sets before and after inlining. *) Definition agree_regs (F: meminj) (ctx: context) (rs rs': regset) := - (forall r, Ple r ctx.(mreg) -> val_inject F rs#r rs'#(sreg ctx r)) + (forall r, Ple r ctx.(mreg) -> Val.inject F rs#r rs'#(sreg ctx r)) /\(forall r, Plt ctx.(mreg) r -> rs#r = Vundef). Definition val_reg_charact (F: meminj) (ctx: context) (rs': regset) (v: val) (r: reg) := - (Plt ctx.(mreg) r /\ v = Vundef) \/ (Ple r ctx.(mreg) /\ val_inject F v rs'#(sreg ctx r)). + (Plt ctx.(mreg) r /\ v = Vundef) \/ (Ple r ctx.(mreg) /\ Val.inject F v rs'#(sreg ctx r)). Remark Plt_Ple_dec: forall p q, {Plt p q} + {Ple q p}. @@ -138,7 +138,7 @@ Proof. Qed. Lemma agree_val_reg: - forall F ctx rs rs' r, agree_regs F ctx rs rs' -> val_inject F rs#r rs'#(sreg ctx r). + forall F ctx rs rs' r, agree_regs F ctx rs rs' -> Val.inject F rs#r rs'#(sreg ctx r). Proof. intros. exploit agree_val_reg_gen; eauto. instantiate (1 := r). intros [[A B] | [A B]]. rewrite B; auto. @@ -146,7 +146,7 @@ Proof. Qed. Lemma agree_val_regs: - forall F ctx rs rs' rl, agree_regs F ctx rs rs' -> val_list_inject F rs##rl rs'##(sregs ctx rl). + forall F ctx rs rs' rl, agree_regs F ctx rs rs' -> Val.inject_list F rs##rl rs'##(sregs ctx rl). Proof. induction rl; intros; simpl. constructor. constructor; auto. apply agree_val_reg; auto. Qed. @@ -154,7 +154,7 @@ Qed. Lemma agree_set_reg: forall F ctx rs rs' r v v', agree_regs F ctx rs rs' -> - val_inject F v v' -> + Val.inject F v v' -> Ple r ctx.(mreg) -> agree_regs F ctx (rs#r <- v) (rs'#(sreg ctx r) <- v'). Proof. @@ -218,7 +218,7 @@ Qed. Lemma agree_regs_init_regs: forall F ctx rl vl vl', - val_list_inject F vl vl' -> + Val.inject_list F vl vl' -> (forall r, In r rl -> Ple r ctx.(mreg)) -> agree_regs F ctx (init_regs vl rl) (init_regs vl' (sregs ctx rl)). Proof. @@ -389,7 +389,7 @@ Proof. (* register *) assert (rs'#(sreg ctx r) = rs#r). exploit Genv.find_funct_inv; eauto. intros [b EQ]. - assert (A: val_inject F rs#r rs'#(sreg ctx r)). eapply agree_val_reg; eauto. + assert (A: Val.inject F rs#r rs'#(sreg ctx r)). eapply agree_val_reg; eauto. rewrite EQ in A; inv A. inv H1. rewrite DOMAIN in H5. inv H5. auto. apply FUNCTIONS with fd. @@ -411,7 +411,7 @@ Lemma tr_annot_arg: forall a v, eval_annot_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v -> exists v', eval_annot_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (sannotarg ctx a) v' - /\ val_inject F v v'. + /\ Val.inject F v v'. Proof. intros until m'; intros MG AG SP MI. induction 1; simpl. - exists rs'#(sreg ctx x); split. constructor. eapply agree_val_reg; eauto. @@ -424,7 +424,7 @@ Proof. simpl. econstructor; eauto. rewrite Int.add_zero_l; auto. intros (v' & A & B). exists v'; split; auto. constructor. simpl. rewrite Int.add_zero_l; auto. - econstructor; split. constructor. simpl. econstructor; eauto. rewrite ! Int.add_zero_l; auto. -- assert (val_inject F (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)). +- assert (Val.inject F (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)). { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. inv MG. econstructor. eauto. rewrite Int.add_zero; auto. } @@ -436,7 +436,7 @@ Proof. inv MG. econstructor. eauto. rewrite Int.add_zero; auto. - destruct IHeval_annot_arg1 as (v1 & A1 & B1). destruct IHeval_annot_arg2 as (v2 & A2 & B2). - econstructor; split. eauto with aarg. apply val_longofwords_inject; auto. + econstructor; split. eauto with aarg. apply Val.longofwords_inject; auto. Qed. Lemma tr_annot_args: @@ -448,7 +448,7 @@ Lemma tr_annot_args: forall al vl, eval_annot_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl -> exists vl', eval_annot_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (map (sannotarg ctx) al) vl' - /\ val_list_inject F vl vl'. + /\ Val.inject_list F vl vl'. Proof. induction 5; simpl. - exists (@nil val); split; constructor. @@ -856,7 +856,7 @@ Inductive match_states: state -> state -> Prop := | match_call_states: forall stk fd args m stk' fd' args' m' F (MS: match_stacks F m m' stk stk' (Mem.nextblock m')) (FD: transf_fundef fenv fd = OK fd') - (VINJ: val_list_inject F args args') + (VINJ: Val.inject_list F args args') (MINJ: Mem.inject F m m'), match_states (Callstate stk fd args m) (Callstate stk' fd' args' m') @@ -876,7 +876,7 @@ Inductive match_states: state -> state -> Prop := (State stk' f' (Vptr sp' Int.zero) pc' rs' m') | match_return_states: forall stk v m stk' v' m' F (MS: match_stacks F m m' stk stk' (Mem.nextblock m')) - (VINJ: val_inject F v v') + (VINJ: Val.inject F v v') (MINJ: Mem.inject F m m'), match_states (Returnstate stk v m) (Returnstate stk' v' m') @@ -884,7 +884,7 @@ Inductive match_states: state -> state -> Prop := (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs') (RET: ctx.(retinfo) = Some rinfo) (AT: f'.(fn_code)!pc' = Some(inline_return ctx or rinfo)) - (VINJ: match or with None => v = Vundef | Some r => val_inject F v rs'#(sreg ctx r) end) + (VINJ: match or with None => v = Vundef | Some r => Val.inject F v rs'#(sreg ctx r) end) (MINJ: Mem.inject F m m') (VB: Mem.valid_block m' sp') (PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize)) @@ -1120,7 +1120,7 @@ Proof. (* jumptable *) exploit tr_funbody_inv; eauto. intros TR; inv TR. - assert (val_inject F rs#arg rs'#(sreg ctx arg)). eapply agree_val_reg; eauto. + assert (Val.inject F rs#arg rs'#(sreg ctx arg)). eapply agree_val_reg; eauto. rewrite H0 in H2; inv H2. left; econstructor; split. eapply plus_one. eapply exec_Ijumptable; eauto. diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index 8beff265..770648b1 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -840,7 +840,7 @@ Lemma default_needs_of_condition_sound: eval_condition cond args2 m2 = Some b. Proof. intros. apply eval_condition_inj with (f := inject_id) (m1 := m1) (vl1 := args1); auto. - apply val_list_inject_lessdef. apply lessdef_vagree_list. auto. + apply val_inject_list_lessdef. apply lessdef_vagree_list. auto. Qed. Lemma default_needs_of_operation_sound: @@ -866,7 +866,7 @@ Proof. eassumption. auto. auto. auto. instantiate (1 := op). intros. apply val_inject_lessdef; auto. apply val_inject_lessdef. instantiate (1 := Vptr sp Int.zero). instantiate (1 := Vptr sp Int.zero). auto. - apply val_list_inject_lessdef; eauto. + apply val_inject_list_lessdef; eauto. eauto. intros (v2 & A & B). exists v2; split; auto. apply vagree_lessdef. apply val_inject_lessdef. auto. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index f4a1935f..7f41512e 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -508,14 +508,14 @@ Qed. (** A variant of [index_contains], up to a memory injection. *) Definition index_contains_inj (j: meminj) (m: mem) (sp: block) (idx: frame_index) (v: val) : Prop := - exists v', index_contains m sp idx v' /\ val_inject j v v'. + exists v', index_contains m sp idx v' /\ Val.inject j v v'. Lemma gss_index_contains_inj: forall j idx m m' sp v v', Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v' = Some m' -> index_valid idx -> Val.has_type v (type_of_index idx) -> - val_inject j v v' -> + Val.inject j v v' -> index_contains_inj j m' sp idx v. Proof. intros. exploit gss_index_contains_base; eauto. intros [v'' [A B]]. @@ -530,7 +530,7 @@ Lemma gss_index_contains_inj': forall j idx m m' sp v v', Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v' = Some m' -> index_valid idx -> - val_inject j v v' -> + Val.inject j v v' -> index_contains_inj j m' sp idx (Val.load_result (chunk_of_type (type_of_index idx)) v). Proof. intros. exploit gss_index_contains_base; eauto. intros [v'' [A B]]. @@ -598,7 +598,7 @@ Hint Resolve store_other_index_contains_inj index_contains_inj_incr: stacking. (** Agreement with Mach register states *) Definition agree_regs (j: meminj) (ls: locset) (rs: regset) : Prop := - forall r, val_inject j (ls (R r)) (rs r). + forall r, Val.inject j (ls (R r)) (rs r). (** Agreement over data stored in memory *) @@ -693,14 +693,14 @@ Definition agree_callee_save (ls ls0: locset) : Prop := Lemma agree_reg: forall j ls rs r, - agree_regs j ls rs -> val_inject j (ls (R r)) (rs r). + agree_regs j ls rs -> Val.inject j (ls (R r)) (rs r). Proof. intros. auto. Qed. Lemma agree_reglist: forall j ls rs rl, - agree_regs j ls rs -> val_list_inject j (reglist ls rl) (rs##rl). + agree_regs j ls rs -> Val.inject_list j (reglist ls rl) (rs##rl). Proof. induction rl; simpl; intros. auto. constructor. eauto with stacking. auto. @@ -713,7 +713,7 @@ Hint Resolve agree_reg agree_reglist: stacking. Lemma agree_regs_set_reg: forall j ls rs r v v', agree_regs j ls rs -> - val_inject j v v' -> + Val.inject j v v' -> agree_regs j (Locmap.set (R r) v ls) (Regmap.set r v' rs). Proof. intros; red; intros. @@ -725,7 +725,7 @@ Qed. Lemma agree_regs_set_regs: forall j rl vl vl' ls rs, agree_regs j ls rs -> - val_list_inject j vl vl' -> + Val.inject_list j vl vl' -> agree_regs j (Locmap.setlist (map R rl) vl ls) (set_regs rl vl' rs). Proof. induction rl; simpl; intros. @@ -850,7 +850,7 @@ Lemma agree_frame_set_local: forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'', agree_frame j ls ls0 m sp m' sp' parent retaddr -> slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true -> - val_inject j v v' -> + Val.inject j v v' -> Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_local ofs ty)) v' = Some m'' -> agree_frame j (Locmap.set (S Local ofs ty) v ls) ls0 m sp m'' sp' parent retaddr. Proof. @@ -889,7 +889,7 @@ Lemma agree_frame_set_outgoing: forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'', agree_frame j ls ls0 m sp m' sp' parent retaddr -> slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true -> - val_inject j v v' -> + Val.inject j v v' -> Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_arg ofs ty)) v' = Some m'' -> agree_frame j (Locmap.set (S Outgoing ofs ty) v ls) ls0 m sp m'' sp' parent retaddr. Proof. @@ -981,7 +981,7 @@ Lemma agree_frame_parallel_stores: forall j ls ls0 m sp m' sp' parent retaddr chunk addr addr' v v' m1 m1', agree_frame j ls ls0 m sp m' sp' parent retaddr -> Mem.inject j m m' -> - val_inject j addr addr' -> + Val.inject j addr addr' -> Mem.storev chunk m addr v = Some m1 -> Mem.storev chunk m' addr' v' = Some m1' -> agree_frame j ls ls0 m1 sp m1' sp' parent retaddr. @@ -1669,7 +1669,7 @@ Hypothesis mkindex_val: index_contains_inj j m sp (mkindex (number r)) (ls0 (R r)). Definition agree_unused (ls0: locset) (rs: regset) : Prop := - forall r, ~(mreg_within_bounds b r) -> val_inject j (ls0 (R r)) (rs r). + forall r, ~(mreg_within_bounds b r) -> Val.inject j (ls0 (R r)) (rs r). Lemma restore_callee_save_regs_correct: forall l rs k, @@ -1681,7 +1681,7 @@ Lemma restore_callee_save_regs_correct: (State cs fb (Vptr sp Int.zero) (restore_callee_save_regs bound number mkindex ty fe l k) rs m) E0 (State cs fb (Vptr sp Int.zero) k rs' m) - /\ (forall r, In r l -> val_inject j (ls0 (R r)) (rs' r)) + /\ (forall r, In r l -> Val.inject j (ls0 (R r)) (rs' r)) /\ (forall r, ~(In r l) -> rs' r = rs r) /\ agree_unused ls0 rs'. Proof. @@ -1734,7 +1734,7 @@ Lemma restore_callee_save_correct: E0 (State cs fb (Vptr sp' Int.zero) k rs' m') /\ (forall r, In r int_callee_save_regs \/ In r float_callee_save_regs -> - val_inject j (ls0 (R r)) (rs' r)) + Val.inject j (ls0 (R r)) (rs' r)) /\ (forall r, ~(In r int_callee_save_regs) -> ~(In r float_callee_save_regs) -> @@ -1986,7 +1986,7 @@ Qed. Lemma match_stacks_parallel_stores: forall j m m' chunk addr addr' v v' m1 m1', Mem.inject j m m' -> - val_inject j addr addr' -> + Val.inject j addr addr' -> Mem.storev chunk m addr v = Some m1 -> Mem.storev chunk m' addr' v' = Some m1' -> forall cs cs' sg bound bound', @@ -2327,7 +2327,7 @@ Hypothesis AGCS: agree_callee_save ls (parent_locset cs). Lemma transl_external_argument: forall l, In l (loc_arguments sg) -> - exists v, extcall_arg rs m' (parent_sp cs') l v /\ val_inject j (ls l) v. + exists v, extcall_arg rs m' (parent_sp cs') l v /\ Val.inject j (ls l) v. Proof. intros. assert (loc_argument_acceptable l). apply loc_arguments_acceptable with sg; auto. @@ -2354,7 +2354,7 @@ Lemma transl_external_arguments_rec: forall locs, incl locs (loc_arguments sg) -> exists vl, - list_forall2 (extcall_arg rs m' (parent_sp cs')) locs vl /\ val_list_inject j ls##locs vl. + list_forall2 (extcall_arg rs m' (parent_sp cs')) locs vl /\ Val.inject_list j ls##locs vl. Proof. induction locs; simpl; intros. exists (@nil val); split. constructor. constructor. @@ -2366,7 +2366,7 @@ Qed. Lemma transl_external_arguments: exists vl, extcall_arguments rs m' (parent_sp cs') sg vl /\ - val_list_inject j (ls ## (loc_arguments sg)) vl. + Val.inject_list j (ls ## (loc_arguments sg)) vl. Proof. unfold extcall_arguments. apply transl_external_arguments_rec. @@ -2402,7 +2402,7 @@ Lemma transl_annot_arg_correct: (forall sl ofs ty, In (S sl ofs ty) (params_of_annot_arg a) -> slot_within_bounds b sl ofs ty) -> exists v', eval_annot_arg ge rs (Vptr sp' Int.zero) m' (transl_annot_arg fe a) v' - /\ val_inject j v v'. + /\ Val.inject j v v'. Proof. Local Opaque fe offset_of_index. induction 1; simpl; intros VALID BOUNDS. @@ -2424,7 +2424,7 @@ Local Transparent fe. eapply agree_bounds; eauto. eapply Mem.valid_access_perm. eapply Mem.load_valid_access; eauto. - econstructor; split; eauto with aarg. unfold Val.add. rewrite ! Int.add_zero_l. econstructor. eapply agree_inj; eauto. auto. -- assert (val_inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)). +- assert (Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)). { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) eqn:FS; auto. econstructor. eapply (proj1 GINJ); eauto. rewrite Int.add_zero; auto. } @@ -2436,7 +2436,7 @@ Local Transparent fe. - destruct IHeval_annot_arg1 as (v1 & A1 & B1); auto using in_or_app. destruct IHeval_annot_arg2 as (v2 & A2 & B2); auto using in_or_app. exists (Val.longofwords v1 v2); split; auto with aarg. - apply val_longofwords_inject; auto. + apply Val.longofwords_inject; auto. Qed. Lemma transl_annot_args_correct: @@ -2446,7 +2446,7 @@ Lemma transl_annot_args_correct: (forall sl ofs ty, In (S sl ofs ty) (params_of_annot_args al) -> slot_within_bounds b sl ofs ty) -> exists vl', eval_annot_args ge rs (Vptr sp' Int.zero) m' (List.map (transl_annot_arg fe) al) vl' - /\ val_list_inject j vl vl'. + /\ Val.inject_list j vl vl'. Proof. induction 1; simpl; intros VALID BOUNDS. - exists (@nil val); split; constructor. @@ -2618,7 +2618,7 @@ Proof. - (* Lop *) assert (exists v', eval_operation ge (Vptr sp' Int.zero) (transl_op (make_env (function_bounds f)) op) rs0##args m' = Some v' - /\ val_inject j v v'). + /\ Val.inject j v v'). eapply eval_operation_inject; eauto. eapply match_stacks_preserves_globals; eauto. eapply agree_inj; eauto. eapply agree_reglist; eauto. @@ -2636,7 +2636,7 @@ Proof. - (* Lload *) assert (exists a', eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' - /\ val_inject j a a'). + /\ Val.inject j a a'). eapply eval_addressing_inject; eauto. eapply match_stacks_preserves_globals; eauto. eapply agree_inj; eauto. eapply agree_reglist; eauto. @@ -2654,7 +2654,7 @@ Proof. - (* Lstore *) assert (exists a', eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' - /\ val_inject j a a'). + /\ Val.inject j a a'). eapply eval_addressing_inject; eauto. eapply match_stacks_preserves_globals; eauto. eapply agree_inj; eauto. eapply agree_reglist; eauto. diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 90d7f270..85e7a360 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -554,7 +554,7 @@ Qed. Lemma symbol_address_inject: forall j id ofs, meminj_preserves_globals j -> kept id -> - val_inject j (Genv.symbol_address ge id ofs) (Genv.symbol_address tge id ofs). + Val.inject j (Genv.symbol_address ge id ofs) (Genv.symbol_address tge id ofs). Proof. intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. exploit symbols_inject_2; eauto. intros (b' & TFS & INJ). rewrite TFS. @@ -564,17 +564,17 @@ Qed. (** Semantic preservation *) Definition regset_inject (f: meminj) (rs rs': regset): Prop := - forall r, val_inject f rs#r rs'#r. + forall r, Val.inject f rs#r rs'#r. Lemma regs_inject: - forall f rs rs', regset_inject f rs rs' -> forall l, val_list_inject f rs##l rs'##l. + forall f rs rs', regset_inject f rs rs' -> forall l, Val.inject_list f rs##l rs'##l. Proof. induction l; simpl. constructor. constructor; auto. Qed. Lemma set_reg_inject: forall f rs rs' r v v', - regset_inject f rs rs' -> val_inject f v v' -> + regset_inject f rs rs' -> Val.inject f v v' -> regset_inject f (rs#r <- v) (rs'#r <- v'). Proof. intros; red; intros. rewrite ! Regmap.gsspec. destruct (peq r0 r); auto. @@ -593,7 +593,7 @@ Proof. Qed. Lemma init_regs_inject: - forall f args args', val_list_inject f args args' -> + forall f args args', Val.inject_list f args args' -> forall params, regset_inject f (init_regs args params) (init_regs args' params). Proof. @@ -689,13 +689,13 @@ Inductive match_states: state -> state -> Prop := | match_states_call: forall s fd args m ts targs tm j (STACKS: match_stacks j s ts (Mem.nextblock m) (Mem.nextblock tm)) (KEPT: forall id, ref_fundef fd id -> kept id) - (ARGINJ: val_list_inject j args targs) + (ARGINJ: Val.inject_list j args targs) (MEMINJ: Mem.inject j m tm), match_states (Callstate s fd args m) (Callstate ts fd targs tm) | match_states_return: forall s res m ts tres tm j (STACKS: match_stacks j s ts (Mem.nextblock m) (Mem.nextblock tm)) - (RESINJ: val_inject j res tres) + (RESINJ: Val.inject j res tres) (MEMINJ: Mem.inject j m tm), match_states (Returnstate s res m) (Returnstate ts tres tm). @@ -706,10 +706,10 @@ Lemma external_call_inject: external_call ef ge vargs m1 t vres m2 -> (forall id, In id (globals_external ef) -> kept id) -> Mem.inject f m1 m1' -> - val_list_inject f vargs vargs' -> + Val.inject_list f vargs vargs' -> exists f', exists vres', exists m2', external_call ef tge vargs' m1' t vres' m2' - /\ val_inject f' vres vres' + /\ Val.inject f' vres vres' /\ Mem.inject f' m2 m2' /\ Mem.unchanged_on (loc_unmapped f) m1 m2 /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2' @@ -751,7 +751,7 @@ Lemma eval_annot_arg_inject: (forall id, In id (globals_of_annot_arg a) -> kept id) -> exists v', eval_annot_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' a v' - /\ val_inject j v v'. + /\ Val.inject j v v'. Proof. induction 1; intros SP GL RS MI K; simpl in K. - exists rs'#x; split; auto. constructor. @@ -762,7 +762,7 @@ Proof. - simpl in H. exploit Mem.load_inject; eauto. rewrite Zplus_0_r. intros (v' & A & B). exists v'; auto with aarg. - econstructor; split; eauto with aarg. simpl. econstructor; eauto. rewrite Int.add_zero; auto. -- assert (val_inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)). +- assert (Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)). { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. exploit symbols_inject_2; eauto. intros (b' & A & B). rewrite A. @@ -776,7 +776,7 @@ Proof. - destruct IHeval_annot_arg1 as (v1' & A1 & B1); eauto using in_or_app. destruct IHeval_annot_arg2 as (v2' & A2 & B2); eauto using in_or_app. exists (Val.longofwords v1' v2'); split; auto with aarg. - apply val_longofwords_inject; auto. + apply Val.longofwords_inject; auto. Qed. Lemma eval_annot_args_inject: @@ -789,7 +789,7 @@ Lemma eval_annot_args_inject: (forall id, In id (globals_of_annot_args al) -> kept id) -> exists vl', eval_annot_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' al vl' - /\ val_list_inject j vl vl'. + /\ Val.inject_list j vl vl'. Proof. induction 1; intros. - exists (@nil val); split; constructor. @@ -814,7 +814,7 @@ Proof. - (* op *) assert (A: exists tv, eval_operation tge (Vptr tsp Int.zero) op trs##args tm = Some tv - /\ val_inject j v tv). + /\ Val.inject j v tv). { apply eval_operation_inj with (ge1 := ge) (m1 := m) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. @@ -832,7 +832,7 @@ Proof. - (* load *) assert (A: exists ta, eval_addressing tge (Vptr tsp Int.zero) addr trs##args = Some ta - /\ val_inject j a ta). + /\ Val.inject j a ta). { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. apply KEPT. red. exists pc, (Iload chunk addr args dst pc'); auto. @@ -847,7 +847,7 @@ Proof. - (* store *) assert (A: exists ta, eval_addressing tge (Vptr tsp Int.zero) addr trs##args = Some ta - /\ val_inject j a ta). + /\ Val.inject j a ta). { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. apply KEPT. red. exists pc, (Istore chunk addr args src pc'); auto. @@ -961,7 +961,7 @@ Proof. econstructor; split. eapply exec_function_internal; eauto. eapply match_states_regular with (j := j'); eauto. - apply init_regs_inject; auto. apply val_list_inject_incr with j; auto. + apply init_regs_inject; auto. apply val_inject_list_incr with j; auto. - (* external function *) exploit external_call_inject; eauto. diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 8720ce50..28934ce9 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -923,7 +923,7 @@ Proof. rewrite JBELOW in H by auto. eapply inj_of_bc_inv; eauto. rewrite H; congruence. } - assert (VMTOP: forall v v', val_inject j' v v' -> vmatch bc' v Vtop). + assert (VMTOP: forall v v', Val.inject j' v v' -> vmatch bc' v Vtop). { intros. inv H; constructor. eapply PMTOP; eauto. } diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index ff3ccfa1..b4c1df61 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -3690,7 +3690,7 @@ Proof. Qed. Lemma vmatch_inj: - forall bc v x, vmatch bc v x -> val_inject (inj_of_bc bc) v v. + forall bc v x, vmatch bc v x -> Val.inject (inj_of_bc bc) v v. Proof. induction 1; econstructor. eapply pmatch_inj; eauto. rewrite Int.add_zero; auto. @@ -3698,7 +3698,7 @@ Proof. Qed. Lemma vmatch_list_inj: - forall bc vl xl, list_forall2 (vmatch bc) vl xl -> val_list_inject (inj_of_bc bc) vl vl. + forall bc vl xl, list_forall2 (vmatch bc) vl xl -> Val.inject_list (inj_of_bc bc) vl vl. Proof. induction 1; constructor. eapply vmatch_inj; eauto. auto. Qed. @@ -3761,7 +3761,7 @@ Proof. Qed. Lemma vmatch_inj_top: - forall bc v v', val_inject (inj_of_bc bc) v v' -> vmatch bc v Vtop. + forall bc v v', Val.inject (inj_of_bc bc) v v' -> vmatch bc v Vtop. Proof. intros. inv H; constructor. eapply pmatch_inj_top; eauto. Qed. |