diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-02 19:50:21 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-02 19:50:21 +0100 |
| commit | f7ea436ac282b6a4a8ddb2281b6e1d86eee46286 (patch) | |
| tree | da7eb4202324967b61bd6993998feefc0455215b /backend/CSE2.v | |
| parent | 036fc22224c8d171a90b608f6146e742a51e0a25 (diff) | |
| download | compcert-kvx-f7ea436ac282b6a4a8ddb2281b6e1d86eee46286.tar.gz compcert-kvx-f7ea436ac282b6a4a8ddb2281b6e1d86eee46286.zip | |
swap predicate
Diffstat (limited to 'backend/CSE2.v')
| -rw-r--r-- | backend/CSE2.v | 8 |
1 files changed, 8 insertions, 0 deletions
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 |