aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-03 08:58:01 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-03 08:58:01 +0100
commitc4f88ed5581ffb71e7ed5824c7503e8ce08165df (patch)
tree74794f389a24da51281d12456d3018c62929693f
parenta398b5750ceeeab90a44b2e1d34fe6d5ff8b1f08 (diff)
downloadcompcert-kvx-c4f88ed5581ffb71e7ed5824c7503e8ce08165df.tar.gz
compcert-kvx-c4f88ed5581ffb71e7ed5824c7503e8ce08165df.zip
globals alias analysis for x86
-rw-r--r--backend/CSE2.v2
-rw-r--r--backend/CSE2proof.v67
-rw-r--r--test/cse2/globals.c8
3 files changed, 67 insertions, 10 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v
index f5ff8748..5b0556aa 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -288,6 +288,8 @@ Definition may_overlap chunk addr args chunk' addr' args' :=
if peq base base'
then negb (can_swap_accesses_ofs ofs' chunk' ofs chunk)
else true
+ | (Aglobal symb ofs), (Aglobal symb' ofs'),
+ nil, nil => peq symb symb'
| _, _, _, _ => true
end.
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index e65d9194..ada0eb00 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -716,7 +716,6 @@ Section MEMORY_WRITE.
Variable m m2 : mem.
Variable chunkw chunkr : memory_chunk.
Variable base : val.
- Variable ofsw ofsr : Z.
Lemma size_chunk_bounded :
forall chunk, 0 <= size_chunk chunk <= max_chunk_size.
@@ -726,13 +725,15 @@ Section MEMORY_WRITE.
Qed.
Variable addrw addrr valw valr : val.
-
+ Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
+ Hypothesis READ : Mem.loadv chunkr m addrr = Some valr.
+
+ Section INDEXED_AWAY.
+ Variable ofsw ofsr : Z.
Hypothesis ADDRW : eval_addressing genv sp
(Aindexed ofsw) (base :: nil) = Some addrw.
Hypothesis ADDRR : eval_addressing genv sp
(Aindexed ofsr) (base :: nil) = Some addrr.
- Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
- Hypothesis READ : Mem.loadv chunkr m addrr = Some valr.
Lemma load_store_away1 :
forall RANGEW : 0 <= ofsw <= Ptrofs.modulus - max_chunk_size,
@@ -800,6 +801,47 @@ Section MEMORY_WRITE.
apply load_store_away1.
all: tauto.
Qed.
+ End INDEXED_AWAY.
+
+ Section DIFFERENT_GLOBALS.
+ Variable ofsw ofsr : ptrofs.
+ Hypothesis symw symr : ident.
+ Hypothesis ADDRW : eval_addressing genv sp
+ (Aglobal symw ofsw) nil = Some addrw.
+ Hypothesis ADDRR : eval_addressing genv sp
+ (Aglobal symr ofsr) nil = Some addrr.
+
+ Lemma load_store_diff_globals :
+ symw <> symr ->
+ Mem.loadv chunkr m2 addrr = Some valr.
+ Proof.
+ intros.
+ unfold eval_addressing in *.
+ destruct Archi.ptr64 eqn:PTR64; simpl in *.
+ rewrite PTR64 in *.
+ 2: simpl in *; discriminate.
+ unfold Genv.symbol_address in *.
+ unfold Genv.find_symbol in *.
+ destruct ((Genv.genv_symb genv) ! symw) as [bw |] eqn:SYMW; inv ADDRW.
+ 2: simpl in STORE; discriminate.
+ destruct ((Genv.genv_symb genv) ! symr) as [br |] eqn:SYMR; inv ADDRR.
+ 2: simpl in READ; discriminate.
+ assert (br <> bw).
+ {
+ intro EQ.
+ subst br.
+ assert (symr = symw).
+ {
+ eapply Genv.genv_vars_inj; eauto.
+ }
+ congruence.
+ }
+ rewrite <- READ.
+ eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := bw).
+ - exact STORE.
+ - left. assumption.
+ Qed.
+ End DIFFERENT_GLOBALS.
End MEMORY_WRITE.
Lemma kill_mem_sound :
@@ -848,6 +890,7 @@ Proof.
apply op_depends_on_memory_correct; auto.
}
destruct addr; destruct addr0; simpl; trivial.
+ { (* Aindexed / Aindexed *)
destruct args as [ | base [ | ]]; simpl; trivial.
destruct args0 as [ | base0 [ | ]]; simpl; trivial.
destruct (peq (forward_move rel base) base0); simpl; trivial.
@@ -857,12 +900,16 @@ Proof.
erewrite forward_move_rs in * by exact SEM.
destruct (eval_addressing genv sp (Aindexed z0) ((rs # base) :: nil)) eqn:ADDR0; simpl; trivial.
symmetry.
- eapply load_store_away.
- - exact ADDR.
- - exact ADDR0.
- - exact STORE.
- - congruence.
- - assumption.
+ eapply load_store_away; eauto.
+ }
+ { (* Aglobal / Aglobal *)
+ destruct args; destruct args0; simpl; trivial.
+ destruct (peq i i1); simpl; trivial.
+ simpl in *.
+ destruct (eval_addressing genv sp (Aglobal i1 i2) nil) eqn:ADDR1; simpl; trivial.
+ symmetry.
+ eapply load_store_diff_globals; eauto.
+ }
Qed.
End SOUNDNESS.
diff --git a/test/cse2/globals.c b/test/cse2/globals.c
new file mode 100644
index 00000000..c6dd59cd
--- /dev/null
+++ b/test/cse2/globals.c
@@ -0,0 +1,8 @@
+int glob1, glob2;
+
+void toto() {
+ if (glob1 > 4) {
+ glob2 ++;
+ glob1 --;
+ }
+}