diff options
| -rw-r--r-- | backend/CSE2.v | 8 | ||||
| -rw-r--r-- | backend/CSE2proof.v | 32 |
2 files changed, 27 insertions, 13 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 diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 55ec653c..6d5496fd 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -704,14 +704,6 @@ Section MEMORY_WRITE. Variable base : val. Variable ofsw ofsr : Z. - Definition max_chunk_size := 8. - (* - Hypothesis RANGEW : 0 <= ofsw <= 18446744073709551608. - Hypothesis RANGER : 0 <= ofsr <= 18446744073709551608. - *) - Hypothesis RANGEW : 0 <= ofsw <= Ptrofs.modulus - max_chunk_size. - Hypothesis RANGER : 0 <= ofsr <= Ptrofs.modulus - max_chunk_size. - Lemma size_chunk_bounded : forall chunk, 0 <= size_chunk chunk <= max_chunk_size. Proof. @@ -719,10 +711,6 @@ Section MEMORY_WRITE. destruct chunk; simpl; lia. Qed. - Hypothesis no_overlap: - ofsw + size_chunk chunkw <= ofsr - \/ ofsr + size_chunk chunkr <= ofsw. - Variable addrw addrr valw valr : val. Hypothesis ADDRW : eval_addressing genv sp @@ -732,9 +720,15 @@ Section MEMORY_WRITE. Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. Hypothesis READ : Mem.loadv chunkr m addrr = Some valr. - Theorem load_store_away : + Lemma load_store_away1 : + forall RANGEW : 0 <= ofsw <= Ptrofs.modulus - max_chunk_size, + forall RANGER : 0 <= ofsr <= Ptrofs.modulus - max_chunk_size, + forall SWAPPABLE : ofsw + size_chunk chunkw <= ofsr + \/ ofsr + size_chunk chunkr <= ofsw, Mem.loadv chunkr m2 addrr = Some valr. Proof. + intros. + pose proof (size_chunk_bounded chunkr) as size_chunkr_bounded. pose proof (size_chunk_bounded chunkw) as size_chunkw_bounded. unfold max_chunk_size in size_chunkr_bounded, size_chunkw_bounded. @@ -779,6 +773,18 @@ Section MEMORY_WRITE. all: intuition lia. Qed. + + Theorem load_store_away : + can_swap_accesses_ofs ofsr chunkr ofsw chunkw = true -> + Mem.loadv chunkr m2 addrr = Some valr. + Proof. + intro SWAP. + unfold can_swap_accesses_ofs in SWAP. + repeat rewrite andb_true_iff in SWAP. + repeat rewrite orb_true_iff in SWAP. + repeat rewrite Z.leb_le in SWAP. + apply load_store_away1; intuition. + Qed. End MEMORY_WRITE. Lemma kill_mem_sound : |