diff options
| -rw-r--r-- | arm/Asm.v | 14 | ||||
| -rw-r--r-- | arm/Asmgenproof.v | 8 | ||||
| -rw-r--r-- | arm/ConstpropOpproof.v | 4 | ||||
| -rw-r--r-- | arm/Op.v | 20 | ||||
| -rw-r--r-- | arm/SelectOpproof.v | 4 | ||||
| -rw-r--r-- | arm/ValueAOp.v | 2 | ||||
| -rw-r--r-- | backend/Constpropproof.v | 6 | ||||
| -rw-r--r-- | backend/Selectionproof.v | 2 | ||||
| -rw-r--r-- | backend/ValueDomain.v | 11 | ||||
| -rw-r--r-- | common/Globalenvs.v | 17 | ||||
| -rw-r--r-- | ia32/Asm.v | 16 | ||||
| -rw-r--r-- | ia32/Asmgenproof.v | 8 | ||||
| -rw-r--r-- | ia32/Asmgenproof1.v | 4 | ||||
| -rw-r--r-- | ia32/ConstpropOpproof.v | 31 | ||||
| -rw-r--r-- | ia32/Op.v | 44 | ||||
| -rw-r--r-- | ia32/SelectOpproof.v | 20 | ||||
| -rw-r--r-- | ia32/ValueAOp.v | 2 | ||||
| -rw-r--r-- | powerpc/Asm.v | 26 | ||||
| -rw-r--r-- | powerpc/Asmgenproof.v | 8 | ||||
| -rw-r--r-- | powerpc/Asmgenproof1.v | 47 | ||||
| -rw-r--r-- | powerpc/ConstpropOpproof.v | 19 | ||||
| -rw-r--r-- | powerpc/Op.v | 36 | ||||
| -rw-r--r-- | powerpc/SelectOpproof.v | 23 | ||||
| -rw-r--r-- | powerpc/ValueAOp.v | 2 |
24 files changed, 156 insertions, 218 deletions
@@ -493,12 +493,6 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool := must survive the execution of the pseudo-instruction. *) -Definition symbol_offset (id: ident) (ofs: int) : val := - match Genv.find_symbol ge id with - | Some b => Vptr b ofs - | None => Vundef - end. - Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome := match i with | Padd r1 r2 so => @@ -514,11 +508,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | None => Stuck end | Pbsymb id sg => - Next (rs#PC <- (symbol_offset id Int.zero)) m + Next (rs#PC <- (Genv.symbol_address ge id Int.zero)) m | Pbreg r sg => Next (rs#PC <- (rs#r)) m | Pblsymb id sg => - Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (symbol_offset id Int.zero)) m + Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (Genv.symbol_address ge id Int.zero)) m | Pblreg r sg => Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (rs#r)) m | Pbic r1 r2 so => @@ -649,7 +643,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Plabel lbl => Next (nextinstr rs) m | Ploadsymbol r1 lbl ofs => - Next (nextinstr (rs#r1 <- (symbol_offset lbl ofs))) m + Next (nextinstr (rs#r1 <- (Genv.symbol_address ge lbl ofs))) m | Pbtbl r tbl => match rs#r with | Vint n => @@ -763,7 +757,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) # IR14 <- Vzero # IR13 <- Vzero in Genv.init_mem p = Some m0 -> diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 19f5687..cfe4f54 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -662,7 +662,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. @@ -730,7 +730,7 @@ Opaque loadind. eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. - simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. reflexivity. + simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. reflexivity. traceEq. econstructor; eauto. split. Simpl. eapply parent_sp_def; eauto. @@ -944,13 +944,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/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 7cf5879..00ea8bc 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/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 @@ -177,12 +177,6 @@ Global Opaque eq_shift eq_condition eq_operation eq_addressing. (** * 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, @@ -219,7 +213,7 @@ 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) @@ -397,7 +391,7 @@ Proof with (try exact I). destruct op; simpl; simpl in H0; FuncInv; try subst v... congruence. destruct (Float.is_single_dec f); red; 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... @@ -714,7 +708,7 @@ Lemma eval_operation_preserved: Proof. intros. unfold eval_operation; destruct op; auto. - unfold symbol_address. rewrite agree_on_symbols; auto. + unfold Genv.symbol_address. rewrite agree_on_symbols; auto. Qed. Lemma eval_addressing_preserved: @@ -739,7 +733,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. @@ -902,7 +896,7 @@ Lemma eval_addressing_inj: exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. Proof. assert (UNUSED: 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)). exact symbol_address_inj. intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. apply Values.val_add_inject; auto. @@ -1032,9 +1026,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/arm/SelectOpproof.v b/arm/SelectOpproof.v index d10e7fc..4b89119 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -114,7 +114,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. @@ -150,7 +150,7 @@ 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 x. rewrite Val.add_assoc. rewrite Int.add_commut. auto. Qed. diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v index 037b22e..b312361 100644 --- a/arm/ValueAOp.v +++ b/arm/ValueAOp.v @@ -149,7 +149,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. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index d88d6e4..ecae5dc 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -133,7 +133,7 @@ Proof. destruct (areg ae r); auto. destruct p; auto. predSpec Int.eq Int.eq_spec ofs Int.zero; intros; auto. subst ofs. exploit vmatch_ptr_gl; eauto. intros LD'. inv LD'; try discriminate. - rewrite H1 in FF. unfold symbol_address in FF. + rewrite H1 in FF. unfold Genv.symbol_address in FF. simpl. rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|]; try discriminate. simpl in FF. rewrite dec_eq_true in FF. @@ -162,8 +162,8 @@ Proof. - (* pointer *) destruct p; try discriminate. + (* global *) - inv H. exists (symbol_address ge id ofs); split. - unfold symbol_address. rewrite <- symbols_preserved. reflexivity. + inv H. exists (Genv.symbol_address ge id ofs); split. + unfold Genv.symbol_address. rewrite <- symbols_preserved. reflexivity. eapply vmatch_ptr_gl; eauto. + (* stack *) inv H. exists (Vptr sp ofs); split. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index c292b49..175b025 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -380,7 +380,7 @@ Proof. exists (Val.longofwords (Vint (Int64.hiword i)) (Vint (Int64.loword i))); split. eapply eval_Eop. constructor. EvalOp. simpl; eauto. constructor. EvalOp. simpl; eauto. constructor. auto. simpl. rewrite Int64.ofwords_recompose. auto. - rewrite <- symbols_preserved. fold (symbol_address tge i i0). apply eval_addrsymbol. + rewrite <- symbols_preserved. fold (Genv.symbol_address tge i i0). apply eval_addrsymbol. apply eval_addrstack. (* Eunop *) exploit IHeval_expr; eauto. intros [v1' [A B]]. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 2ece8cd..c8431bb 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -1075,15 +1075,12 @@ Definition genv_match (ge: genv) : Prop := (forall id b, Genv.find_symbol ge id = Some b <-> bc b = BCglob id) /\(forall b, Plt b (Genv.genv_next ge) -> bc b <> BCinvalid /\ bc b <> BCstack). -Definition symbol_address (ge: genv) (id: ident) (ofs: int) : val := - match Genv.find_symbol ge id with Some b => Vptr b ofs | None => Vundef end. - Lemma symbol_address_sound: forall ge id ofs, genv_match ge -> - vmatch (symbol_address ge id ofs) (Ptr (Gl id ofs)). + vmatch (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)). Proof. - intros. unfold symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. + intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. constructor. constructor. apply H; auto. constructor. Qed. @@ -1092,9 +1089,9 @@ Lemma vmatch_ptr_gl: forall ge v id ofs, genv_match ge -> vmatch v (Ptr (Gl id ofs)) -> - Val.lessdef v (symbol_address ge id ofs). + Val.lessdef v (Genv.symbol_address ge id ofs). Proof. - intros. unfold symbol_address. inv H0. + intros. unfold Genv.symbol_address. inv H0. - inv H3. replace (Genv.find_symbol ge id) with (Some b). constructor. symmetry. apply H; auto. - constructor. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 4e155e3..3b077e0 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -102,6 +102,16 @@ Record t: Type := mkgenv { Definition find_symbol (ge: t) (id: ident) : option block := PTree.get id ge.(genv_symb). +(** [symbol_address ge id ofs] returns a pointer into the block associated + with [id], at byte offset [ofs]. [Vundef] is returned if no block is associated + to [id]. *) + +Definition symbol_address (ge: t) (id: ident) (ofs: int) : val := + match find_symbol ge id with + | Some b => Vptr b ofs + | None => Vundef + end. + (** [find_funct_ptr ge b] returns the function description associated with the given address. *) @@ -267,6 +277,13 @@ End GLOBALENV_PRINCIPLES. (** ** Properties of the operations over global environments *) +Theorem shift_symbol_address: + forall ge id ofs n, + symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n). +Proof. + intros. unfold symbol_address. destruct (find_symbol ge id); auto. +Qed. + Theorem find_funct_inv: forall ge v f, find_funct ge v = Some f -> exists b, v = Vptr b Int.zero. @@ -275,12 +275,6 @@ Fixpoint label_pos (lbl: label) (pos: Z) (c: code) {struct c} : option Z := 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. - (** Evaluating an addressing mode *) Definition eval_addrmode (a: addrmode) (rs: regset) : val := @@ -296,7 +290,7 @@ Definition eval_addrmode (a: addrmode) (rs: regset) : val := end) (match const with | inl ofs => Vint ofs - | inr(id, ofs) => symbol_offset id ofs + | inr(id, ofs) => Genv.symbol_address ge id ofs end)) end. @@ -477,7 +471,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmov_ri rd n => Next (nextinstr_nf (rs#rd <- (Vint n))) m | Pmov_ra rd id => - Next (nextinstr_nf (rs#rd <- (symbol_offset id Int.zero))) m + Next (nextinstr_nf (rs#rd <- (Genv.symbol_address ge id Int.zero))) m | Pmov_rm rd a => exec_load Mint32 m a rs rd | Pmov_mr a r1 => @@ -631,7 +625,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pjmp_l lbl => goto_label f lbl rs m | Pjmp_s id sg => - Next (rs#PC <- (symbol_offset id Int.zero)) m + Next (rs#PC <- (Genv.symbol_address ge id Int.zero)) m | Pjmp_r r sg => Next (rs#PC <- (rs r)) m | Pjcc cond lbl => @@ -656,7 +650,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | _ => Stuck end | Pcall_s id sg => - Next (rs#RA <- (Val.add rs#PC Vone) #PC <- (symbol_offset id Int.zero)) m + Next (rs#RA <- (Val.add rs#PC Vone) #PC <- (Genv.symbol_address ge id Int.zero)) m | Pcall_r r sg => Next (rs#RA <- (Val.add rs#PC Vone) #PC <- (rs r)) m | Pret => @@ -806,7 +800,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) # RA <- Vzero # ESP <- Vzero in initial_state p (State rs0 m0). diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index fa8ce6c..881375f 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -613,7 +613,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. @@ -665,7 +665,7 @@ Opaque loadind. econstructor; eauto. apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto. eapply agree_change_sp; eauto. eapply parent_sp_def; eauto. - rewrite Pregmap.gss. unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. + rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. - (* Mbuiltin *) inv AT. monadInv H3. @@ -900,13 +900,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/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 6f2aee5..b3c815b 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -381,11 +381,11 @@ Proof. monadInv H. rewrite (ireg_of_eq _ _ EQ); rewrite (ireg_of_eq _ _ EQ1); simpl. apply Val.add_lessdef; auto. apply Val.add_lessdef; auto. (* global *) - inv H. simpl. unfold symbol_address, symbol_offset. + inv H. simpl. unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); simpl; auto. repeat rewrite Int.add_zero. auto. (* based *) monadInv H. rewrite (ireg_of_eq _ _ EQ). simpl. - unfold symbol_address, symbol_offset. destruct (Genv.find_symbol ge i); simpl; auto. + unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); simpl; auto. rewrite Int.add_zero. rewrite Val.add_commut. auto. (* basedscaled *) monadInv H. rewrite (ireg_of_eq _ _ EQ). unfold eval_addrmode. diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v index 8a05534..d9eea2b 100644 --- a/ia32/ConstpropOpproof.v +++ b/ia32/ConstpropOpproof.v @@ -46,7 +46,7 @@ Hypothesis MATCH: ematch bc e ae. Lemma match_G: forall r id ofs, - AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef e#r (symbol_address ge id ofs). + AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef e#r (Genv.symbol_address ge id ofs). Proof. intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH. Qed. @@ -79,7 +79,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 @@ -103,13 +103,6 @@ Proof. - 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 -> @@ -120,15 +113,15 @@ 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. +- rewrite Genv.shift_symbol_address. econstructor; split. eauto. apply Val.add_lessdef; auto. - econstructor; split; eauto. rewrite Int.add_zero_l. change (Vptr sp (Int.add n ofs)) with (Val.add (Vptr sp n) (Vint ofs)). apply Val.add_lessdef; auto. -- econstructor; split; eauto. rewrite Int.add_assoc. rewrite shift_symbol_address. +- econstructor; split; eauto. rewrite Int.add_assoc. rewrite Genv.shift_symbol_address. rewrite Val.add_assoc. apply Val.add_lessdef; auto. - econstructor; split; eauto. fold (Val.add (Vint n1) e#r2). rewrite (Val.add_commut (Vint n1)). - rewrite shift_symbol_address. apply Val.add_lessdef; auto. - rewrite Int.add_commut. rewrite shift_symbol_address. apply Val.add_lessdef; auto. + rewrite Genv.shift_symbol_address. apply Val.add_lessdef; auto. + rewrite Int.add_commut. rewrite Genv.shift_symbol_address. apply Val.add_lessdef; auto. - econstructor; split; eauto. rewrite Int.add_zero_l. rewrite Int.add_assoc. change (Vptr sp (Int.add n1 (Int.add n2 ofs))) with (Val.add (Vptr sp n1) (Vint (Int.add n2 ofs))). @@ -138,10 +131,10 @@ Proof. change (Vptr sp (Int.add (Int.add n2 n1) ofs)) with (Val.add (Val.add (Vint n1) (Vptr sp n2)) (Vint ofs)). apply Val.add_lessdef; auto. apply Val.add_lessdef; auto. -- econstructor; split; eauto. rewrite shift_symbol_address. +- econstructor; split; eauto. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. apply Val.add_lessdef; auto. rewrite Val.add_commut. apply Val.add_lessdef; auto. -- econstructor; split; eauto. rewrite shift_symbol_address. +- econstructor; split; eauto. rewrite Genv.shift_symbol_address. rewrite (Val.add_commut e#r1). rewrite ! Val.add_assoc. apply Val.add_lessdef; auto. rewrite Val.add_commut. apply Val.add_lessdef; auto. - fold (Val.add (Vint n1) e#r2). econstructor; split; eauto. @@ -150,13 +143,13 @@ Proof. - econstructor; split; eauto. rewrite ! Val.add_assoc. apply Val.add_lessdef; eauto. - econstructor; split; eauto. rewrite Int.add_assoc. - rewrite shift_symbol_address. apply Val.add_lessdef; auto. + rewrite Genv.shift_symbol_address. apply Val.add_lessdef; auto. - econstructor; split; eauto. - rewrite shift_symbol_address. rewrite ! Val.add_assoc. apply Val.add_lessdef; auto. + rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. apply Val.add_lessdef; auto. rewrite Val.add_commut; auto. - econstructor; split; eauto. -- econstructor; split; eauto. rewrite shift_symbol_address. auto. -- econstructor; split; eauto. rewrite shift_symbol_address. rewrite Int.mul_commut; auto. +- econstructor; split; eauto. rewrite Genv.shift_symbol_address. auto. +- econstructor; split; eauto. rewrite Genv.shift_symbol_address. rewrite Int.mul_commut; auto. - econstructor; eauto. Qed. @@ -156,12 +156,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, @@ -193,11 +187,11 @@ Definition eval_addressing | Aindexed2scaled sc ofs, v1::v2::nil => Some(Val.add v1 (Val.add (Val.mul v2 (Vint sc)) (Vint ofs))) | Aglobal s ofs, nil => - Some (symbol_address genv s ofs) + Some (Genv.symbol_address genv s ofs) | Abased s ofs, v1::nil => - Some (Val.add (symbol_address genv s ofs) v1) + Some (Val.add (Genv.symbol_address genv s ofs) v1) | Abasedscaled sc s ofs, v1::nil => - Some (Val.add (symbol_address genv s ofs) (Val.mul v1 (Vint sc))) + Some (Val.add (Genv.symbol_address genv s ofs) (Val.mul v1 (Vint sc))) | Ainstack ofs, nil => Some(Val.add sp (Vint ofs)) | _, _ => None @@ -210,7 +204,7 @@ Definition eval_operation | Omove, v1::nil => Some v1 | Ointconst n, nil => Some (Vint n) | Ofloatconst n, nil => Some (Vfloat n) - | Oindirectsymbol id, nil => Some (symbol_address genv id Int.zero) + | Oindirectsymbol id, nil => Some (Genv.symbol_address genv id Int.zero) | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1) | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1) | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1) @@ -368,11 +362,11 @@ Proof with (try exact I). destruct v0... destruct v1... destruct v1... destruct v0... destruct v0... destruct v1... destruct v1... - unfold symbol_address; destruct (Genv.find_symbol genv i)... - unfold symbol_address; destruct (Genv.find_symbol genv i)... - unfold symbol_address; destruct (Genv.find_symbol genv i)... destruct v0... + unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)... + unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)... + unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)... destruct v0... destruct v0... - unfold symbol_address; destruct (Genv.find_symbol genv i0)... destruct v0... + unfold Genv.symbol_address; destruct (Genv.find_symbol genv i0)... destruct v0... destruct sp... Qed. @@ -387,7 +381,7 @@ 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 v0... destruct v0... destruct v0... @@ -568,10 +562,10 @@ Proof. rewrite !Val.add_assoc; auto. rewrite !Val.add_assoc; auto. 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. - unfold symbol_address. destruct (Genv.find_symbol ge i0); auto. + unfold Genv.symbol_address. destruct (Genv.find_symbol ge i0); auto. rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. rewrite Val.add_assoc. auto. Qed. @@ -645,7 +639,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. @@ -656,7 +650,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. @@ -689,7 +683,7 @@ Lemma eval_addressing_preserved: eval_addressing ge2 sp addr vl = eval_addressing ge1 sp addr vl. Proof. intros. - unfold eval_addressing, symbol_address; destruct addr; try rewrite agree_on_symbols; + unfold eval_addressing, Genv.symbol_address; destruct addr; try rewrite agree_on_symbols; reflexivity. Qed. @@ -699,7 +693,7 @@ Lemma eval_operation_preserved: Proof. intros. unfold eval_operation; destruct op; auto. - unfold symbol_address. rewrite agree_on_symbols. auto. + unfold Genv.symbol_address. rewrite agree_on_symbols. auto. apply eval_addressing_preserved. Qed. @@ -715,7 +709,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. @@ -992,9 +986,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/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index b528a72..0fd6f7b 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -113,14 +113,14 @@ 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. exists (symbol_address ge id ofs); split; auto. + intros. unfold addrsymbol. exists (Genv.symbol_address ge id ofs); split; auto. destruct (symbol_is_external id). predSpec Int.eq Int.eq_spec ofs Int.zero. subst. EvalOp. EvalOp. econstructor. EvalOp. simpl; eauto. econstructor. simpl. - unfold symbol_address. destruct (Genv.find_symbol ge id); auto. + unfold Genv.symbol_address. destruct (Genv.find_symbol ge id); auto. simpl. rewrite Int.add_commut. rewrite Int.add_zero. auto. EvalOp. Qed. @@ -142,12 +142,6 @@ Proof. TrivialExists. Qed. -Lemma shift_symbol_address: - forall id ofs n, symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n). -Proof. - intros. unfold symbol_address. destruct (Genv.find_symbol); auto. -Qed. - Theorem eval_addimm: forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)). Proof. @@ -170,13 +164,13 @@ Proof. subst. TrivialExists. simpl. rewrite Val.add_permut_4. auto. subst. TrivialExists. simpl. rewrite Val.add_assoc. decEq; decEq. rewrite Val.add_permut. auto. subst. TrivialExists. simpl. rewrite Val.add_permut_4. rewrite <- Val.add_permut. rewrite <- Val.add_assoc. auto. - subst. TrivialExists. simpl. rewrite shift_symbol_address. + subst. TrivialExists. simpl. rewrite Genv.shift_symbol_address. rewrite Val.add_commut. rewrite Val.add_assoc. decEq. decEq. apply Val.add_commut. - subst. TrivialExists. simpl. rewrite shift_symbol_address. rewrite Val.add_assoc. + subst. TrivialExists. simpl. rewrite Genv.shift_symbol_address. rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut. - subst. TrivialExists. simpl. rewrite shift_symbol_address. rewrite Val.add_commut. + subst. TrivialExists. simpl. rewrite Genv.shift_symbol_address. rewrite Val.add_commut. rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut. - subst. TrivialExists. simpl. rewrite shift_symbol_address. + subst. TrivialExists. simpl. rewrite Genv.shift_symbol_address. rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut. subst. TrivialExists. simpl. rewrite Val.add_permut. rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut. diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v index f3e2194..58b945f 100644 --- a/ia32/ValueAOp.v +++ b/ia32/ValueAOp.v @@ -128,7 +128,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. 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. |