summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--arm/Asm.v14
-rw-r--r--arm/Asmgenproof.v8
-rw-r--r--arm/ConstpropOpproof.v4
-rw-r--r--arm/Op.v20
-rw-r--r--arm/SelectOpproof.v4
-rw-r--r--arm/ValueAOp.v2
-rw-r--r--backend/Constpropproof.v6
-rw-r--r--backend/Selectionproof.v2
-rw-r--r--backend/ValueDomain.v11
-rw-r--r--common/Globalenvs.v17
-rw-r--r--ia32/Asm.v16
-rw-r--r--ia32/Asmgenproof.v8
-rw-r--r--ia32/Asmgenproof1.v4
-rw-r--r--ia32/ConstpropOpproof.v31
-rw-r--r--ia32/Op.v44
-rw-r--r--ia32/SelectOpproof.v20
-rw-r--r--ia32/ValueAOp.v2
-rw-r--r--powerpc/Asm.v26
-rw-r--r--powerpc/Asmgenproof.v8
-rw-r--r--powerpc/Asmgenproof1.v47
-rw-r--r--powerpc/ConstpropOpproof.v19
-rw-r--r--powerpc/Op.v36
-rw-r--r--powerpc/SelectOpproof.v23
-rw-r--r--powerpc/ValueAOp.v2
24 files changed, 156 insertions, 218 deletions
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.
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.
diff --git a/ia32/Asm.v b/ia32/Asm.v
index f03ea75..2e5b8b9 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -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.
diff --git a/ia32/Op.v b/ia32/Op.v
index 5420607..e46c740 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -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.