From f7ea436ac282b6a4a8ddb2281b6e1d86eee46286 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 2 Mar 2020 19:50:21 +0100 Subject: swap predicate --- backend/CSE2.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index b7665097..a03e02a4 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -266,6 +266,14 @@ Definition kill_reg (dst : reg) (rel : RELATION.t) := PTree.filter1 (fun x => negb (kill_sym_val dst x)) (PTree.remove dst rel). +Definition max_chunk_size := 8. + +Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw := + (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - max_chunk_size)) + && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - max_chunk_size)) + && ((ofsw + size_chunk chunkw <=? ofsr) || + (ofsr + size_chunk chunkr <=? ofsw)). + Definition kill_sym_val_mem (sv: sym_val) := match sv with | SMove _ => false -- cgit From a398b5750ceeeab90a44b2e1d34fe6d5ff8b1f08 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 06:13:05 +0100 Subject: with indexed/indexed alias analysis for x86 --- backend/CSE2.v | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) (limited to 'backend/CSE2.v') 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)) -- cgit From c4f88ed5581ffb71e7ed5824c7503e8ce08165df Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 08:58:01 +0100 Subject: globals alias analysis for x86 --- backend/CSE2.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'backend/CSE2.v') 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. -- cgit From af7afc0a388986a94f21d2657cc13b823d456781 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 09:39:03 +0100 Subject: offsets in globals for x86 --- backend/CSE2.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 5b0556aa..9c45b476 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -289,7 +289,10 @@ Definition may_overlap chunk addr args chunk' addr' args' := then negb (can_swap_accesses_ofs ofs' chunk' ofs chunk) else true | (Aglobal symb ofs), (Aglobal symb' ofs'), - nil, nil => peq symb symb' + nil, nil => + if peq symb symb' + then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) + else false | _, _, _, _ => true end. -- cgit From 74efac13484e4767f793cf9ccc94835825ca30ba Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 12:27:58 +0100 Subject: CSE2 alias analysis for Risc-V --- backend/CSE2.v | 25 +------------------------ 1 file changed, 1 insertion(+), 24 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 9c45b476..8142ee5d 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -6,7 +6,7 @@ David Monniaux, CNRS, VERIMAG Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. -Require Import Memory Registers Op RTL Maps. +Require Import Memory Registers Op RTL Maps CSE2deps. (* Static analysis *) @@ -265,14 +265,6 @@ Definition kill_sym_val (dst : reg) (sv : sym_val) := Definition kill_reg (dst : reg) (rel : RELATION.t) := PTree.filter1 (fun x => negb (kill_sym_val dst x)) (PTree.remove dst rel). - -Definition max_chunk_size := 8. - -Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw := - (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - max_chunk_size)) - && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - max_chunk_size)) - && ((ofsw + size_chunk chunkw <=? ofsr) || - (ofsr + size_chunk chunkr <=? ofsw)). Definition kill_sym_val_mem (sv: sym_val) := match sv with @@ -281,21 +273,6 @@ 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 - | (Aglobal symb ofs), (Aglobal symb' ofs'), - nil, nil => - if peq symb symb' - then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) - else false - | _, _, _, _ => true - end. - Definition kill_sym_val_store chunk addr args (sv: sym_val) := match sv with | SMove _ => false -- cgit