From 3fa79790e617d87584598746296e626e0ce3b256 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 24 May 2014 09:46:07 +0000 Subject: Refactoring: move symbol_offset into Genv. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asm.v | 26 ++++++++++--------------- powerpc/Asmgenproof.v | 8 ++++---- powerpc/Asmgenproof1.v | 47 +++++++++++++++++----------------------------- powerpc/ConstpropOpproof.v | 19 ++++++------------- powerpc/Op.v | 36 +++++++++++++++-------------------- powerpc/SelectOpproof.v | 23 ++++++++--------------- powerpc/ValueAOp.v | 2 +- 7 files changed, 61 insertions(+), 100 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 7a75d8f..aba78d4 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -376,12 +376,6 @@ Definition gpr_or_zero (rs: regset) (r: ireg) := Variable ge: genv. -Definition symbol_offset (id: ident) (ofs: int) : val := - match Genv.find_symbol ge id with - | Some b => Vptr b ofs - | None => Vundef - end. - (** The two functions below axiomatize how the linker processes symbolic references [symbol + offset] and splits their actual values into two 16-bit halves. *) @@ -395,8 +389,8 @@ Parameter high_half: val -> val. Axiom low_high_half: forall id ofs, - Val.add (low_half (symbol_offset id ofs)) (high_half (symbol_offset id ofs)) - = symbol_offset id ofs. + Val.add (low_half (Genv.symbol_address ge id ofs)) (high_half (Genv.symbol_address ge id ofs)) + = Genv.symbol_address ge id ofs. (** The other axioms we take is that the results of the [low_half] and [high_half] functions are of type [Tint], @@ -421,7 +415,7 @@ Parameter small_data_area_offset: genv -> ident -> int -> val. Axiom small_data_area_addressing: forall id ofs, symbol_is_small_data id ofs = true -> - small_data_area_offset ge id ofs = symbol_offset id ofs. + small_data_area_offset ge id ofs = Genv.symbol_address ge id ofs. Parameter symbol_is_rel_data: ident -> int -> bool. @@ -436,10 +430,10 @@ Parameter symbol_is_rel_data: ident -> int -> bool. Definition const_low (c: constant) := match c with | Cint n => Vint n - | Csymbol_low id ofs => low_half (symbol_offset id ofs) + | Csymbol_low id ofs => low_half (Genv.symbol_address ge id ofs) | Csymbol_high id ofs => Vundef | Csymbol_sda id ofs => small_data_area_offset ge id ofs - | Csymbol_rel_low id ofs => low_half (symbol_offset id ofs) + | Csymbol_rel_low id ofs => low_half (Genv.symbol_address ge id ofs) | Csymbol_rel_high id ofs => Vundef end. @@ -447,10 +441,10 @@ Definition const_high (c: constant) := match c with | Cint n => Vint (Int.shl n (Int.repr 16)) | Csymbol_low id ofs => Vundef - | Csymbol_high id ofs => high_half (symbol_offset id ofs) + | Csymbol_high id ofs => high_half (Genv.symbol_address ge id ofs) | Csymbol_sda id ofs => Vundef | Csymbol_rel_low id ofs => Vundef - | Csymbol_rel_high id ofs => high_half (symbol_offset id ofs) + | Csymbol_rel_high id ofs => high_half (Genv.symbol_address ge id ofs) end. (** The semantics is purely small-step and defined as a function @@ -597,9 +591,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | _ => Stuck end | Pbl ident sg => - Next (rs#LR <- (Val.add rs#PC Vone) #PC <- (symbol_offset ident Int.zero)) m + Next (rs#LR <- (Val.add rs#PC Vone) #PC <- (Genv.symbol_address ge ident Int.zero)) m | Pbs ident sg => - Next (rs#PC <- (symbol_offset ident Int.zero)) m + Next (rs#PC <- (Genv.symbol_address ge ident Int.zero)) m | Pblr => Next (rs#PC <- (rs#LR)) m | Pbt bit lbl => @@ -900,7 +894,7 @@ Inductive initial_state (p: program): state -> Prop := let ge := Genv.globalenv p in let rs0 := (Pregmap.init Vundef) - # PC <- (symbol_offset ge p.(prog_main) Int.zero) + # PC <- (Genv.symbol_address ge p.(prog_main) Int.zero) # LR <- Vzero # GPR1 <- Vzero in initial_state p (State rs0 m0). diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 5c99231..879d752 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -642,7 +642,7 @@ Opaque loadind. left; econstructor; split. apply plus_one. eapply exec_step_internal. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. - simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. eauto. + simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto. econstructor; eauto. econstructor; eauto. eapply agree_sp_def; eauto. @@ -733,7 +733,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. eapply functions_transl; eauto. eapply find_instr_tail. repeat (eapply code_tail_next_int; auto). eauto. - simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. traceEq. + simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. traceEq. (* match states *) econstructor; eauto. assert (AG3: agree rs (Vptr stk soff) rs3). @@ -972,13 +972,13 @@ Proof. econstructor; split. econstructor. eapply Genv.init_mem_transf_partial; eauto. - replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero) + replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Int.zero) with (Vptr fb Int.zero). econstructor; eauto. constructor. apply Mem.extends_refl. split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. - unfold symbol_offset. + unfold Genv.symbol_address. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. unfold ge; rewrite H1. auto. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 2436e2f..cfeb823 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -103,42 +103,30 @@ Proof. rewrite Int.sub_idem. apply Int.add_zero. Qed. -Lemma add_zero_symbol_offset: - forall ge id ofs, - Val.add Vzero (symbol_offset ge id ofs) = symbol_offset ge id ofs. +Lemma add_zero_symbol_address: + forall (ge: genv) id ofs, + Val.add Vzero (Genv.symbol_address ge id ofs) = Genv.symbol_address ge id ofs. Proof. - unfold symbol_offset; intros. destruct (Genv.find_symbol ge id); auto. + unfold Genv.symbol_address; intros. destruct (Genv.find_symbol ge id); auto. simpl. rewrite Int.add_zero; auto. Qed. Lemma csymbol_high_low: - forall ge id ofs, - Val.add (high_half (symbol_offset ge id ofs)) (low_half (symbol_offset ge id ofs)) - = symbol_offset ge id ofs. + forall (ge: genv) id ofs, + Val.add (high_half (Genv.symbol_address ge id ofs)) (low_half (Genv.symbol_address ge id ofs)) + = Genv.symbol_address ge id ofs. Proof. intros. rewrite Val.add_commut. apply low_high_half. Qed. Lemma csymbol_high_low_2: - forall ge id ofs rel, + forall (ge: genv) id ofs rel, Val.add (const_high ge (csymbol_high id ofs rel)) - (const_low ge (csymbol_low id ofs rel)) = symbol_offset ge id ofs. + (const_low ge (csymbol_low id ofs rel)) = Genv.symbol_address ge id ofs. Proof. intros. destruct rel; apply csymbol_high_low. Qed. -(* -Lemma csymbol_sda_eq: - forall ge id ofs, - symbol_is_small_data id ofs = true -> - Val.add Vzero (const_low ge (Csymbol_sda id ofs)) = symbol_offset ge id ofs. -Proof. - intros. unfold const_low. rewrite small_data_area_addressing by auto. - unfold symbol_offset. - destruct (Genv.find_symbol ge id); simpl; auto. rewrite Int.add_zero; auto. -Qed. -*) - (** Useful properties of the GPR0 registers. *) Lemma gpr_or_zero_not_zero: @@ -859,18 +847,17 @@ Opaque Int.eq. destruct (loadimm_correct x i k rs m) as [rs' [A [B C]]]. exists rs'. auto with asmgen. (* Oaddrsymbol *) - change (symbol_address ge i i0) with (symbol_offset ge i i0). - set (v' := symbol_offset ge i i0). + set (v' := Genv.symbol_address ge i i0). destruct (symbol_is_small_data i i0) eqn:SD. (* small data *) Opaque Val.add. econstructor; split. apply exec_straight_one; simpl; reflexivity. - split. Simpl. rewrite small_data_area_addressing by auto. apply add_zero_symbol_offset. + split. Simpl. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address. intros; Simpl. (* not small data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. Simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl. - rewrite Val.add_assoc. rewrite csymbol_high_low_2. apply add_zero_symbol_offset. + rewrite Val.add_assoc. rewrite csymbol_high_low_2. apply add_zero_symbol_address. intros; Simpl. (* Oaddrstack *) destruct (addimm_correct x GPR1 i k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen. @@ -883,14 +870,14 @@ Opaque Val.add. (* small data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. Simpl. rewrite (Val.add_commut (rs x)). f_equal. - rewrite small_data_area_addressing by auto. apply add_zero_symbol_offset. + rewrite small_data_area_addressing by auto. apply add_zero_symbol_address. intros; Simpl. destruct (symbol_is_rel_data i i0). (* relative data *) econstructor; split. eapply exec_straight_three; simpl; reflexivity. split. Simpl. rewrite gpr_or_zero_zero. rewrite gpr_or_zero_not_zero by (eauto with asmgen). Simpl. rewrite Val.add_assoc. rewrite (Val.add_commut (rs x)). f_equal. - rewrite Val.add_assoc. rewrite csymbol_high_low. apply add_zero_symbol_offset. + rewrite Val.add_assoc. rewrite csymbol_high_low. apply add_zero_symbol_address. intros; Simpl. (* absolute data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. @@ -1023,7 +1010,7 @@ Transparent Val.add. destruct (symbol_is_small_data i i0) eqn:SISD; inv TR. (* Aglobal from small data *) apply MK1. unfold const_low. rewrite small_data_area_addressing by auto. - apply add_zero_symbol_offset. + apply add_zero_symbol_address. auto. (* Aglobal general case *) set (rel := symbol_is_rel_data i i0). @@ -1042,7 +1029,7 @@ Transparent Val.add. (* Abased *) destruct (symbol_is_small_data i i0) eqn:SISD. (* Abased from small data *) - set (rs1 := nextinstr (rs#GPR0 <- (symbol_offset ge i i0))). + set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))). exploit (MK2 x GPR0 rs1 k). unfold rs1; Simpl. apply Val.add_commut. intros. unfold rs1; Simpl. @@ -1050,7 +1037,7 @@ Transparent Val.add. exists rs'; split. apply exec_straight_step with rs1 m. unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal. unfold const_low. rewrite small_data_area_addressing; auto. - apply add_zero_symbol_offset. + apply add_zero_symbol_address. reflexivity. assumption. assumption. destruct (symbol_is_rel_data i i0). diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index a28d908..584865a 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -49,7 +49,7 @@ Hypothesis MATCH: ematch bc rs ae. Lemma match_G: forall r id ofs, - AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef rs#r (symbol_address ge id ofs). + AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef rs#r (Genv.symbol_address ge id ofs). Proof. intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH. Qed. @@ -82,7 +82,7 @@ Ltac SimplVM := rewrite E in *; clear H; SimplVM | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] => let E := fresh in - assert (E: Val.lessdef v (Op.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); + assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); clear H; SimplVM | [ H: vmatch _ ?v (Ptr(Stk ?ofs)) |- _ ] => let E := fresh in @@ -436,13 +436,6 @@ Proof. exists v; auto. Qed. -Remark shift_symbol_address: - forall symb ofs n, - Op.symbol_address ge symb (Int.add ofs n) = Val.add (Op.symbol_address ge symb ofs) (Vint n). -Proof. - unfold Op.symbol_address; intros. destruct (Genv.find_symbol ge symb); auto. -Qed. - Lemma addr_strength_reduction_correct: forall addr args vl res, vl = map (fun r => AE.get r ae) args -> @@ -453,8 +446,8 @@ Proof. intros until res. unfold addr_strength_reduction. destruct (addr_strength_reduction_match addr args vl); simpl; intros VL EA; InvApproxRegs; SimplVM; try (inv EA). -- rewrite shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. -- fold (Val.add (Vint n1) rs#r2). rewrite Int.add_commut. rewrite shift_symbol_address. rewrite Val.add_commut. +- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. +- fold (Val.add (Vint n1) rs#r2). rewrite Int.add_commut. rewrite Genv.shift_symbol_address. rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto. - rewrite Int.add_zero_l. change (Vptr sp (Int.add n1 n2)) with (Val.add (Vptr sp n1) (Vint n2)). @@ -467,8 +460,8 @@ Proof. - fold (Val.add (Vint n1) rs#r2). rewrite Val.add_commut. econstructor; split; eauto. - econstructor; split; eauto. -- rewrite shift_symbol_address. econstructor; split; eauto. -- rewrite shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. +- rewrite Genv.shift_symbol_address. econstructor; split; eauto. +- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. - rewrite Int.add_zero_l. change (Vptr sp (Int.add n1 n)) with (Val.add (Vptr sp n1) (Vint n)). econstructor; split; eauto. apply Val.add_lessdef; auto. diff --git a/powerpc/Op.v b/powerpc/Op.v index 3545b18..17cf072 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -147,12 +147,6 @@ Global Opaque eq_condition eq_addressing eq_operation. (** * Evaluation functions *) -Definition symbol_address (F V: Type) (genv: Genv.t F V) (id: ident) (ofs: int) : val := - match Genv.find_symbol genv id with - | Some b => Vptr b ofs - | None => Vundef - end. - (** Evaluation of conditions, operators and addressing modes applied to lists of values. Return [None] when the computation can trigger an error, e.g. integer division by zero. [eval_condition] returns a boolean, @@ -178,13 +172,13 @@ Definition eval_operation | Omove, v1::nil => Some v1 | Ointconst n, nil => Some (Vint n) | Ofloatconst n, nil => Some (Vfloat n) - | Oaddrsymbol s ofs, nil => Some (symbol_address genv s ofs) + | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs) | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs)) | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1) | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1) | Oadd, v1::v2::nil => Some (Val.add v1 v2) | Oaddimm n, v1::nil => Some (Val.add v1 (Vint n)) - | Oaddsymbol s ofs, v1::nil => Some (Val.add (symbol_address genv s ofs) v1) + | Oaddsymbol s ofs, v1::nil => Some (Val.add (Genv.symbol_address genv s ofs) v1) | Osub, v1::v2::nil => Some (Val.sub v1 v2) | Osubimm n, v1::nil => Some (Val.sub (Vint n) v1) | Omul, v1::v2::nil => Some (Val.mul v1 v2) @@ -235,8 +229,8 @@ Definition eval_addressing match addr, vl with | Aindexed n, v1::nil => Some (Val.add v1 (Vint n)) | Aindexed2, v1::v2::nil => Some (Val.add v1 v2) - | Aglobal s ofs, nil => Some (symbol_address genv s ofs) - | Abased s ofs, v1::nil => Some (Val.add (symbol_address genv s ofs) v1) + | Aglobal s ofs, nil => Some (Genv.symbol_address genv s ofs) + | Abased s ofs, v1::nil => Some (Val.add (Genv.symbol_address genv s ofs) v1) | Ainstack ofs, nil => Some(Val.add sp (Vint ofs)) | _, _ => None end. @@ -350,13 +344,13 @@ Proof with (try exact I). congruence. exact I. destruct (Float.is_single_dec f); auto. - unfold symbol_address. destruct (Genv.find_symbol genv i)... + unfold Genv.symbol_address. destruct (Genv.find_symbol genv i)... destruct sp... destruct v0... destruct v0... destruct v0; destruct v1... destruct v0... - unfold symbol_address. destruct (Genv.find_symbol genv i)... destruct v0... + unfold Genv.symbol_address. destruct (Genv.find_symbol genv i)... destruct v0... destruct v0; destruct v1... simpl. destruct (eq_block b b0)... destruct v0... destruct v0; destruct v1... @@ -521,8 +515,8 @@ Lemma eval_offset_addressing: Proof. intros. destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst. rewrite Val.add_assoc; auto. - unfold symbol_address. destruct (Genv.find_symbol ge i); auto. - unfold symbol_address. destruct (Genv.find_symbol ge i); auto. + unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. + unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. rewrite Val.add_assoc. auto. Qed. @@ -615,7 +609,7 @@ Proof. destruct v; simpl in *; inv H1; inv H2. right. apply Int.no_overlap_sound; auto. (* Aglobal *) - unfold symbol_address in *. + unfold Genv.symbol_address in *. destruct (Genv.find_symbol ge i1) eqn:?; inv H2. destruct (Genv.find_symbol ge i) eqn:?; inv H1. destruct (ident_eq i i1). subst. @@ -626,7 +620,7 @@ Proof. rewrite Int.add_commut; rewrite Int.add_zero; auto. left. red; intros; elim n. subst. eapply Genv.genv_vars_inj; eauto. (* Abased *) - unfold symbol_address in *. + unfold Genv.symbol_address in *. destruct (Genv.find_symbol ge i1) eqn:?; simpl in *; try discriminate. destruct v; inv H2. destruct (Genv.find_symbol ge i) eqn:?; inv H1. @@ -655,9 +649,9 @@ Hypothesis agree_on_symbols: forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s. Remark symbol_address_preserved: - forall s ofs, symbol_address ge2 s ofs = symbol_address ge1 s ofs. + forall s ofs, Genv.symbol_address ge2 s ofs = Genv.symbol_address ge1 s ofs. Proof. - unfold symbol_address; intros. rewrite agree_on_symbols; auto. + unfold Genv.symbol_address; intros. rewrite agree_on_symbols; auto. Qed. Lemma eval_operation_preserved: @@ -686,7 +680,7 @@ Variable f: meminj. Hypothesis symbol_address_inj: forall id ofs, - val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs). + val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). Variable m1: mem. Variable m2: mem. @@ -956,9 +950,9 @@ Variable delta: Z. Hypothesis sp_inj: f sp1 = Some(sp2, delta). Remark symbol_address_inject: - forall id ofs, val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs). + forall id ofs, val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). Proof. - intros. unfold symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto. + intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto. exploit (proj1 globals); eauto. intros. econstructor; eauto. rewrite Int.add_zero; auto. Qed. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 1aa889b..cb48d51 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -115,7 +115,7 @@ Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> va Theorem eval_addrsymbol: forall le id ofs, - exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (symbol_address ge id ofs) v. + exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v. Proof. intros. unfold addrsymbol. econstructor; split. EvalOp. simpl; eauto. @@ -154,13 +154,6 @@ Proof. TrivialExists. Qed. -Remark symbol_address_shift: - forall s ofs n, - symbol_address ge s (Int.add ofs n) = Val.add (symbol_address ge s ofs) (Vint n). -Proof. - unfold symbol_address; intros. destruct (Genv.find_symbol ge s); auto. -Qed. - Theorem eval_addimm: forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)). Proof. @@ -170,19 +163,19 @@ Proof. destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Int.add_zero. auto. case (addimm_match a); intros; InvEval; simpl; TrivialExists; simpl. rewrite Int.add_commut. auto. - unfold symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Int.add_commut; auto. + unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Int.add_commut; auto. rewrite Val.add_assoc. rewrite Int.add_commut. auto. subst. rewrite Val.add_assoc. rewrite Int.add_commut. auto. - subst. rewrite Int.add_commut. rewrite symbol_address_shift. rewrite ! Val.add_assoc. f_equal. f_equal. apply Val.add_commut. + subst. rewrite Int.add_commut. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal. f_equal. apply Val.add_commut. Qed. Theorem eval_addsymbol: - forall s ofs, unary_constructor_sound (addsymbol s ofs) (Val.add (symbol_address ge s ofs)). + forall s ofs, unary_constructor_sound (addsymbol s ofs) (Val.add (Genv.symbol_address ge s ofs)). Proof. red; unfold addsymbol; intros until x. case (addsymbol_match a); intros; InvEval; simpl; TrivialExists; simpl. - rewrite symbol_address_shift. auto. - rewrite symbol_address_shift. subst x. rewrite Val.add_assoc. f_equal. f_equal. + rewrite Genv.shift_symbol_address. auto. + rewrite Genv.shift_symbol_address. subst x. rewrite Val.add_assoc. f_equal. f_equal. apply Val.add_commut. Qed. @@ -209,9 +202,9 @@ Proof. simpl. repeat rewrite Val.add_assoc. decEq; decEq. rewrite Val.add_commut. rewrite Val.add_permut. auto. - replace (Val.add x y) with - (Val.add (symbol_address ge s (Int.add ofs n)) (Val.add v1 v0)). + (Val.add (Genv.symbol_address ge s (Int.add ofs n)) (Val.add v1 v0)). apply eval_addsymbol; auto. EvalOp. - subst. rewrite symbol_address_shift. rewrite ! Val.add_assoc. f_equal. + subst. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal. rewrite Val.add_permut. f_equal. apply Val.add_commut. - subst. rewrite Val.add_assoc. apply eval_addsymbol. EvalOp. - subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp. diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index 7f16bb3..77463f4 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -127,7 +127,7 @@ Qed. Lemma symbol_address_sound: forall id ofs, - vmatch bc (symbol_address ge id ofs) (Ptr (Gl id ofs)). + vmatch bc (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)). Proof. intros; apply symbol_address_sound; apply GENV. Qed. -- cgit v1.2.3