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/CSE2proof.v | |
| parent | 036fc22224c8d171a90b608f6146e742a51e0a25 (diff) | |
| download | compcert-kvx-f7ea436ac282b6a4a8ddb2281b6e1d86eee46286.tar.gz compcert-kvx-f7ea436ac282b6a4a8ddb2281b6e1d86eee46286.zip | |
swap predicate
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 32 |
1 files changed, 19 insertions, 13 deletions
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 : |