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 --- arm/Asm.v | 14 ++++---------- arm/Asmgenproof.v | 8 ++++---- arm/ConstpropOpproof.v | 4 ++-- arm/Op.v | 20 +++++++------------- arm/SelectOpproof.v | 4 ++-- arm/ValueAOp.v | 2 +- 6 files changed, 20 insertions(+), 32 deletions(-) (limited to 'arm') diff --git a/arm/Asm.v b/arm/Asm.v index 69f6319..9d3ba5b 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -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 diff --git a/arm/Op.v b/arm/Op.v index 7323abc..b50a7b0 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -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. -- cgit v1.2.3