From 036fc22224c8d171a90b608f6146e742a51e0a25 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 2 Mar 2020 19:10:35 +0100 Subject: works on x86 x86_64 --- backend/CSE2proof.v | 76 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 47 insertions(+), 29 deletions(-) (limited to 'backend/CSE2proof.v') diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 4dd8b054..55ec653c 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -704,12 +704,18 @@ 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 <= 8. + forall chunk, 0 <= size_chunk chunk <= max_chunk_size. Proof. + unfold max_chunk_size. destruct chunk; simpl; lia. Qed. @@ -731,35 +737,47 @@ Section MEMORY_WRITE. Proof. 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. + try change (Ptrofs.modulus - max_chunk_size) with 4294967288 in *. + try change (Ptrofs.modulus - max_chunk_size) with 18446744073709551608 in *. destruct addrr ; simpl in * ; try discriminate. unfold eval_addressing in *. - destruct Archi.ptr64 eqn:PTR64. - { - unfold eval_addressing64 in *. - inv ADDRW. - destruct base; simpl in *; try discriminate. - rewrite PTR64 in *. - inv ADDRR. - rewrite <- READ. - eapply Mem.load_store_other. - exact STORE. - right. - destruct (Ptrofs.unsigned_add_either i0 - (Ptrofs.of_int64 (Int64.repr ofsr))) as [OFSR | OFSR]; - rewrite OFSR. - all: destruct (Ptrofs.unsigned_add_either i0 - (Ptrofs.of_int64 (Int64.repr ofsw))) as [OFSW | OFSW]; - rewrite OFSW. - all: unfold Ptrofs.of_int64. - all: repeat rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; lia). - all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 18446744073709551615; lia). - all: change Ptrofs.modulus with 18446744073709551616. - all: intuition lia. - } - { - destruct base; simpl in *; try discriminate. - } + destruct Archi.ptr64 eqn:PTR64; destruct base; simpl in *; try discriminate. + rewrite PTR64 in *. + + inv ADDRR. + inv ADDRW. + rewrite <- READ. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int (Int.repr ofsr))) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int64 (Int64.repr ofsr))) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int (Int.repr ofsw))) as [OFSW | OFSW]; + rewrite OFSW). + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int64 (Int64.repr ofsw))) as [OFSW | OFSW]; + rewrite OFSW). + + all: unfold Ptrofs.of_int64. + all: unfold Ptrofs.of_int. + + + all: repeat rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia). + all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia). + all: repeat rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; lia). + all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 18446744073709551615; lia). + + all: try change Ptrofs.modulus with 4294967296. + all: try change Ptrofs.modulus with 18446744073709551616. + + all: intuition lia. Qed. End MEMORY_WRITE. -- cgit