diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 06:13:05 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 06:13:05 +0100 |
commit | a398b5750ceeeab90a44b2e1d34fe6d5ff8b1f08 (patch) | |
tree | 5f22972f5e9c74999dab5405757aae9f9631a258 /backend | |
parent | 93bf7e0925b1c11e1874ae5f651970db2bd9823d (diff) | |
download | compcert-kvx-a398b5750ceeeab90a44b2e1d34fe6d5ff8b1f08.tar.gz compcert-kvx-a398b5750ceeeab90a44b2e1d34fe6d5ff8b1f08.zip |
with indexed/indexed alias analysis for x86
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CSE2.v | 26 | ||||
-rw-r--r-- | backend/CSE2proof.v | 4 |
2 files changed, 26 insertions, 4 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index a03e02a4..f5ff8748 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -281,16 +281,38 @@ Definition kill_sym_val_mem (sv: sym_val) := | SLoad _ _ _ => true end. +Definition may_overlap chunk addr args chunk' addr' args' := + match addr, addr', args, args' with + | (Aindexed ofs), (Aindexed ofs'), + (base :: nil), (base' :: nil) => + if peq base base' + then negb (can_swap_accesses_ofs ofs' chunk' ofs chunk) + else true + | _, _, _, _ => true + end. + +Definition kill_sym_val_store chunk addr args (sv: sym_val) := + match sv with + | SMove _ => false + | SOp op _ => op_depends_on_memory op + | SLoad chunk' addr' args' => may_overlap chunk addr args chunk' addr' args' + end. + Definition kill_mem (rel : RELATION.t) := PTree.filter1 (fun x => negb (kill_sym_val_mem x)) rel. - Definition forward_move (rel : RELATION.t) (x : reg) : reg := match rel ! x with | Some (SMove org) => org | _ => x end. +Definition kill_store1 chunk addr args rel := + PTree.filter1 (fun x => negb (kill_sym_val_store chunk addr args x)) rel. + +Definition kill_store chunk addr args rel := + kill_store1 chunk addr (List.map (forward_move rel) args) rel. + Definition move (src dst : reg) (rel : RELATION.t) := PTree.set dst (SMove (forward_move rel src)) (kill_reg dst rel). @@ -403,7 +425,7 @@ Definition apply_instr instr (rel : RELATION.t) : RB.t := | Inop _ | Icond _ _ _ _ | Ijumptable _ _ => Some rel - | Istore _ _ _ _ _ => Some (kill_mem rel) + | Istore chunk addr args _ _ => Some (kill_store chunk addr args rel) | Iop op args dst _ => Some (gen_oper op dst args rel) | Iload chunk addr args dst _ => Some (load chunk addr dst args rel) | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel)) diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index cd9f5f46..e65d9194 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -951,6 +951,7 @@ Definition fmap_sem' := fmap_sem fundef unit ge. Definition subst_arg_ok' := subst_arg_ok fundef unit ge. Definition subst_args_ok' := subst_args_ok fundef unit ge. Definition kill_mem_sound' := kill_mem_sound fundef unit ge. +Definition kill_store_sound' := kill_store_sound fundef unit ge. Lemma sem_rel_b_ge: forall rb1 rb2 : RB.t, @@ -1260,8 +1261,7 @@ Proof. rewrite H. reflexivity. } - apply (kill_store_sound' sp m). - assumption. + eapply (kill_store_sound' sp m); eassumption. (* call *) - econstructor; split. |