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