From 9937f23871513d4bf77db5b541a93f6327365f1e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 11 Dec 2019 19:08:50 +0100 Subject: begin overlap proofs --- mppa_k1c/Asmblockdeps.v | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index c7cfe43c..2b2627e7 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -22,6 +22,8 @@ Require Import Parallelizability. Require Import Asmvliw Permutation. Require Import Chunks. +Require Import Lia. + Open Scope impure. (** Definition of L *) @@ -208,6 +210,47 @@ Definition store_eval (so: store_op) (l: list value) := | _, _ => None end. +Local Open Scope Z. + +Definition no_overlap_segments l1 h1 l2 h2 := + (h1 <=? l2) || (h2 <=? l1). + +Definition in_segment l h x := + (l <=? x) && (x + (in_segment l2 h2 x) = true -> + (no_overlap_segments l1 h1 l2 h2) = false. +Proof. + unfold in_segment, no_overlap_segments. + intros until x. + intros H1 H2. + destruct (andb_true_iff (l1 <=? x) (x + store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m1] = Some (Memstate m2) -> + store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m0] = Some (Memstate m1') -> + store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m1'] = Some (Memstate m2). + Definition goto_label_deps (f: function) (lbl: label) (vpc: val) := match label_pos lbl 0 (fn_blocks f) with | None => None -- cgit From fd1d1f8c981332afad01b36915bc5b06d4066f70 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 12 Dec 2019 15:24:27 +0100 Subject: some subgoal was proved --- mppa_k1c/Asmblockdeps.v | 67 ++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 61 insertions(+), 6 deletions(-) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 2b2627e7..0f534350 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -244,13 +244,68 @@ Proof. rewrite Z.leb_le. lia. Qed. - -Lemma store_swap : forall n1 n2 ofs1 ofs2 vs1 vs2 va m0 m1 m2 m1', - store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m0] = Some (Memstate m1) -> - store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m1] = Some (Memstate m2) -> - store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m0] = Some (Memstate m1') -> - store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m1'] = Some (Memstate m2). +Definition no_overlap_chunks + (ofs1 : offset) (chunk1 : memory_chunk) + (ofs2 : offset) (chunk2 : memory_chunk) := + no_overlap_segments (Ptrofs.unsigned ofs1) + ((Ptrofs.unsigned ofs1) + (size_chunk chunk1)) + (Ptrofs.unsigned ofs2) + ((Ptrofs.unsigned ofs2) + (size_chunk chunk2)). + +Definition same_memory (m m' : mem) := + forall chunk block ofs, + (Mem.load chunk m block ofs) = (Mem.load chunk m' block ofs). + +(* use something like load_store_other *) +Lemma store_swap : forall n1 n2 ofs1 ofs2 vs1 vs2 va m0 m0' m1 m2 m1' m2', + (no_overlap_chunks ofs1 (store_chunk n1) ofs2 (store_chunk n2))=true -> + same_memory m0 m0' -> + store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m0] = Some (Memstate m1) -> + store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m1] = Some (Memstate m2) -> + store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m0'] = Some (Memstate m1') -> + store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m1'] = Some (Memstate m2') -> + same_memory m2 m2'. +Proof. + intros until m2'. + intros NO_OVERLAP SAME STORE0 STORE1 STORE0' STORE1'. + unfold same_memory. + intros rchunk rblock rofs. + unfold no_overlap_chunks in NO_OVERLAP. + unfold no_overlap_segments in NO_OVERLAP. + rewrite orb_true_iff in NO_OVERLAP. + rewrite Z.leb_le in NO_OVERLAP. + rewrite Z.leb_le in NO_OVERLAP. + destruct vs1 as [v1 | ]; simpl in STORE0, STORE1'; try congruence. + destruct vs2 as [v2 | ]; simpl in STORE1, STORE0'; try congruence. + destruct va as [base | ]; try congruence. + unfold exec_store_deps_offset in *. + destruct Ge. + destruct (eval_offset ofs1) as [ i1 |]; try congruence. + destruct (eval_offset ofs2) as [ i2 |]; try congruence. + unfold Mem.storev in *. + unfold Val.offset_ptr in *. + destruct base as [ | | | | | wblock wpofs] in * ; try congruence. + destruct (Mem.store (store_chunk n1) m0 _ _ _) eqn:HS0; try congruence. + inv STORE0. + destruct (Mem.store (store_chunk n2) m1 _ _ _) eqn:HS1; try congruence. + inv STORE1. + destruct (Mem.store (store_chunk n2) m0' _ _ _) eqn:HS0'; try congruence. + inv STORE0'. + destruct (Mem.store (store_chunk n1) m1' _ _ _) eqn:HS1'; try congruence. + inv STORE1'. + destruct (eq_block rblock wblock) as [SAME_BLOCK | DIF_BLOCKS]. + { admit. + } + { (* read from different base block *) + rewrite (Mem.load_store_other (store_chunk n2) m1 wblock (Ptrofs.unsigned (Ptrofs.add wpofs i2)) v2 m2 HS1) by tauto. + rewrite (Mem.load_store_other (store_chunk n1) m0 wblock (Ptrofs.unsigned (Ptrofs.add wpofs i1)) v1 m1 HS0) by tauto. + rewrite (Mem.load_store_other (store_chunk n1) m1' wblock (Ptrofs.unsigned (Ptrofs.add wpofs i1)) v1 m2' HS1') by tauto. + rewrite (Mem.load_store_other (store_chunk n2) m0' wblock (Ptrofs.unsigned (Ptrofs.add wpofs i2)) v2 m1' HS0') by tauto. + apply SAME. + } +Admitted. + Definition goto_label_deps (f: function) (lbl: label) (vpc: val) := match label_pos lbl 0 (fn_blocks f) with | None => None -- cgit From db03f4f3f90d7eab399177fc3f27ac027c10bc9f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 13 Dec 2019 13:10:01 +0100 Subject: progress in chunks --- mppa_k1c/Asmblockdeps.v | 54 +++++++++---------------------------------------- 1 file changed, 9 insertions(+), 45 deletions(-) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 0f534350..c54cc317 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -212,46 +212,13 @@ Definition store_eval (so: store_op) (l: list value) := Local Open Scope Z. -Definition no_overlap_segments l1 h1 l2 h2 := - (h1 <=? l2) || (h2 <=? l1). - -Definition in_segment l h x := - (l <=? x) && (x - (in_segment l2 h2 x) = true -> - (no_overlap_segments l1 h1 l2 h2) = false. -Proof. - unfold in_segment, no_overlap_segments. - intros until x. - intros H1 H2. - destruct (andb_true_iff (l1 <=? x) (x + (disjoint_chunks ofs1 (store_chunk n1) ofs2 (store_chunk n2)) -> same_memory m0 m0' -> store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m0] = Some (Memstate m1) -> store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m1] = Some (Memstate m2) -> @@ -271,11 +238,7 @@ Proof. intros NO_OVERLAP SAME STORE0 STORE1 STORE0' STORE1'. unfold same_memory. intros rchunk rblock rofs. - unfold no_overlap_chunks in NO_OVERLAP. - unfold no_overlap_segments in NO_OVERLAP. - rewrite orb_true_iff in NO_OVERLAP. - rewrite Z.leb_le in NO_OVERLAP. - rewrite Z.leb_le in NO_OVERLAP. + unfold disjoint_chunks in NO_OVERLAP. destruct vs1 as [v1 | ]; simpl in STORE0, STORE1'; try congruence. destruct vs2 as [v2 | ]; simpl in STORE1, STORE0'; try congruence. destruct va as [base | ]; try congruence. @@ -295,7 +258,8 @@ Proof. destruct (Mem.store (store_chunk n1) m1' _ _ _) eqn:HS1'; try congruence. inv STORE1'. destruct (eq_block rblock wblock) as [SAME_BLOCK | DIF_BLOCKS]. - { admit. + { subst rblock. + admit. } { (* read from different base block *) rewrite (Mem.load_store_other (store_chunk n2) m1 wblock (Ptrofs.unsigned (Ptrofs.add wpofs i2)) v2 m2 HS1) by tauto. -- cgit From ce3f5cd4afdd5f5794b9c0a7480947b25e3685d0 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 14 Dec 2019 08:58:12 +0100 Subject: comment out theorem that cannot be proved --- mppa_k1c/Asmblockdeps.v | 62 ++++++++++++++++++++++++++----------------------- 1 file changed, 33 insertions(+), 29 deletions(-) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index c54cc317..4d53763c 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -212,6 +212,12 @@ Definition store_eval (so: store_op) (l: list value) := Local Open Scope Z. +Remark size_chunk_positive: forall chunk, + (size_chunk chunk) > 0. +Proof. + destruct chunk; simpl; lia. +Qed. + Definition disjoint_chunks (ofs1 : offset) (chunk1 : memory_chunk) (ofs2 : offset) (chunk2 : memory_chunk) := @@ -220,56 +226,54 @@ Definition disjoint_chunks ((Ptrofs.unsigned ofs2), ((Ptrofs.unsigned ofs2) + (size_chunk chunk2))). -Definition same_memory (m m' : mem) := - forall chunk block ofs, - (Mem.load chunk m block ofs) = (Mem.load chunk m' block ofs). - +(* THIS CANNOT BE PROVED DUE TO OVERFLOW WRAPPING (* use something like load_store_other *) Lemma store_swap : forall n1 n2 ofs1 ofs2 vs1 vs2 va m0 m0' m1 m2 m1' m2', (disjoint_chunks ofs1 (store_chunk n1) ofs2 (store_chunk n2)) -> - same_memory m0 m0' -> store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m0] = Some (Memstate m1) -> store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m1] = Some (Memstate m2) -> store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m0'] = Some (Memstate m1') -> store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m1'] = Some (Memstate m2') -> - same_memory m2 m2'. + m2 = m2'. Proof. intros until m2'. - intros NO_OVERLAP SAME STORE0 STORE1 STORE0' STORE1'. - unfold same_memory. - intros rchunk rblock rofs. - unfold disjoint_chunks in NO_OVERLAP. + intros DISJOINT STORE0 STORE1 STORE0' STORE1'. + unfold disjoint_chunks in DISJOINT. destruct vs1 as [v1 | ]; simpl in STORE0, STORE1'; try congruence. destruct vs2 as [v2 | ]; simpl in STORE1, STORE0'; try congruence. destruct va as [base | ]; try congruence. unfold exec_store_deps_offset in *. destruct Ge. - destruct (eval_offset ofs1) as [ i1 |]; try congruence. - destruct (eval_offset ofs2) as [ i2 |]; try congruence. + unfold eval_offset in *; simpl in *. unfold Mem.storev in *. unfold Val.offset_ptr in *. destruct base as [ | | | | | wblock wpofs] in * ; try congruence. - destruct (Mem.store (store_chunk n1) m0 _ _ _) eqn:HS0; try congruence. + destruct (Mem.store _ _ _ _) eqn:E0 in STORE0; try congruence. inv STORE0. - destruct (Mem.store (store_chunk n2) m1 _ _ _) eqn:HS1; try congruence. + destruct (Mem.store _ _ _ _) eqn:E1 in STORE1; try congruence. inv STORE1. - destruct (Mem.store (store_chunk n2) m0' _ _ _) eqn:HS0'; try congruence. + destruct (Mem.store _ _ _ _) eqn:E0' in STORE0'; try congruence. inv STORE0'. - destruct (Mem.store (store_chunk n1) m1' _ _ _) eqn:HS1'; try congruence. + destruct (Mem.store _ _ _ _) eqn:E1' in STORE1'; try congruence. inv STORE1'. - destruct (eq_block rblock wblock) as [SAME_BLOCK | DIF_BLOCKS]. - { subst rblock. - admit. - } - { (* read from different base block *) - rewrite (Mem.load_store_other (store_chunk n2) m1 wblock (Ptrofs.unsigned (Ptrofs.add wpofs i2)) v2 m2 HS1) by tauto. - rewrite (Mem.load_store_other (store_chunk n1) m0 wblock (Ptrofs.unsigned (Ptrofs.add wpofs i1)) v1 m1 HS0) by tauto. - rewrite (Mem.load_store_other (store_chunk n1) m1' wblock (Ptrofs.unsigned (Ptrofs.add wpofs i1)) v1 m2' HS1') by tauto. - rewrite (Mem.load_store_other (store_chunk n2) m0' wblock (Ptrofs.unsigned (Ptrofs.add wpofs i2)) v2 m1' HS0') by tauto. - apply SAME. - } -Admitted. - + assert (Some m2 = Some m2'). + 2: congruence. + rewrite <- E1. + rewrite <- E1'. + eapply Mem.store_store_other. + { + right. + pose proof (size_chunk_positive (store_chunk n1)). + pose proof (size_chunk_positive (store_chunk n2)). + destruct (Intv.range_disjoint _ _ DISJOINT) as [DIS | [DIS | DIS]]; + unfold Intv.empty in DIS; simpl in DIS. + 1, 2: lia. + destruct (Ptrofs.unsigned_add_either wpofs ofs1) as [R1 | R1]; rewrite R1; + destruct (Ptrofs.unsigned_add_either wpofs ofs2) as [R2 | R2]; rewrite R2; + try lia. + } +*) + Definition goto_label_deps (f: function) (lbl: label) (vpc: val) := match label_pos lbl 0 (fn_blocks f) with | None => None -- cgit From 34518ae5db9ca7c04d9ce5d90261ede3c9d0e550 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 16 Dec 2019 14:45:56 +0100 Subject: swap stores at disjoint offsets --- mppa_k1c/Asmblockdeps.v | 46 ++++++++++++++++++++++++++++++---------------- 1 file changed, 30 insertions(+), 16 deletions(-) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 4d53763c..759b4396 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -218,6 +218,12 @@ Proof. destruct chunk; simpl; lia. Qed. +Remark size_chunk_small: forall chunk, + (size_chunk chunk) <= 8. +Proof. + destruct chunk; simpl; lia. +Qed. + Definition disjoint_chunks (ofs1 : offset) (chunk1 : memory_chunk) (ofs2 : offset) (chunk2 : memory_chunk) := @@ -226,18 +232,20 @@ Definition disjoint_chunks ((Ptrofs.unsigned ofs2), ((Ptrofs.unsigned ofs2) + (size_chunk chunk2))). -(* THIS CANNOT BE PROVED DUE TO OVERFLOW WRAPPING -(* use something like load_store_other *) -Lemma store_swap : forall n1 n2 ofs1 ofs2 vs1 vs2 va m0 m0' m1 m2 m1' m2', +Definition small_offset_threshold := 18446744073709551608. + +Lemma store_swap : forall n1 n2 ofs1 ofs2 vs1 vs2 va m0 m1 m2 m1' m2', (disjoint_chunks ofs1 (store_chunk n1) ofs2 (store_chunk n2)) -> + (Ptrofs.unsigned ofs1) < small_offset_threshold -> + (Ptrofs.unsigned ofs2) < small_offset_threshold -> store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m0] = Some (Memstate m1) -> store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m1] = Some (Memstate m2) -> - store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m0'] = Some (Memstate m1') -> + store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m0] = Some (Memstate m1') -> store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m1'] = Some (Memstate m2') -> m2 = m2'. Proof. intros until m2'. - intros DISJOINT STORE0 STORE1 STORE0' STORE1'. + intros DISJOINT SMALL1 SMALL2 STORE0 STORE1 STORE0' STORE1'. unfold disjoint_chunks in DISJOINT. destruct vs1 as [v1 | ]; simpl in STORE0, STORE1'; try congruence. destruct vs2 as [v2 | ]; simpl in STORE1, STORE0'; try congruence. @@ -261,18 +269,24 @@ Proof. rewrite <- E1. rewrite <- E1'. eapply Mem.store_store_other. - { - right. - pose proof (size_chunk_positive (store_chunk n1)). - pose proof (size_chunk_positive (store_chunk n2)). - destruct (Intv.range_disjoint _ _ DISJOINT) as [DIS | [DIS | DIS]]; - unfold Intv.empty in DIS; simpl in DIS. - 1, 2: lia. - destruct (Ptrofs.unsigned_add_either wpofs ofs1) as [R1 | R1]; rewrite R1; + 2, 3: eassumption. + + right. + pose proof (size_chunk_positive (store_chunk n1)). + pose proof (size_chunk_positive (store_chunk n2)). + pose proof (size_chunk_small (store_chunk n1)). + pose proof (size_chunk_small (store_chunk n2)). + destruct (Intv.range_disjoint _ _ DISJOINT) as [DIS | [DIS | DIS]]; + unfold Intv.empty in DIS; simpl in DIS. + 1, 2: lia. + pose proof (Ptrofs.unsigned_range ofs1). + pose proof (Ptrofs.unsigned_range ofs2). + unfold small_offset_threshold in *. + destruct (Ptrofs.unsigned_add_either wpofs ofs1) as [R1 | R1]; rewrite R1; destruct (Ptrofs.unsigned_add_either wpofs ofs2) as [R2 | R2]; rewrite R2; - try lia. - } -*) + change Ptrofs.modulus with 18446744073709551616 in *; + lia. +Qed. Definition goto_label_deps (f: function) (lbl: label) (vpc: val) := match label_pos lbl 0 (fn_blocks f) with -- cgit From dc7ba7bf86828da813e60d60dc9627cbd6ddcf0e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 16 Dec 2019 16:45:14 +0100 Subject: swap load and store at disjoint offsets --- mppa_k1c/Asmblockdeps.v | 54 ++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 53 insertions(+), 1 deletion(-) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 759b4396..2cdf9499 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -234,7 +234,8 @@ Definition disjoint_chunks Definition small_offset_threshold := 18446744073709551608. -Lemma store_swap : forall n1 n2 ofs1 ofs2 vs1 vs2 va m0 m1 m2 m1' m2', +Lemma store_store_disjoint_offsets : + forall n1 n2 ofs1 ofs2 vs1 vs2 va m0 m1 m2 m1' m2', (disjoint_chunks ofs1 (store_chunk n1) ofs2 (store_chunk n2)) -> (Ptrofs.unsigned ofs1) < small_offset_threshold -> (Ptrofs.unsigned ofs2) < small_offset_threshold -> @@ -288,6 +289,57 @@ Proof. lia. Qed. +Lemma load_store_disjoint_offsets : + forall n1 n2 tm ofs1 ofs2 vs va m0 m1, + (disjoint_chunks ofs1 (store_chunk n1) ofs2 (load_chunk n2)) -> + (Ptrofs.unsigned ofs1) < small_offset_threshold -> + (Ptrofs.unsigned ofs2) < small_offset_threshold -> + store_eval (OStoreRRO n1 ofs1) [vs; va; Memstate m0] = Some (Memstate m1) -> + load_eval (OLoadRRO n2 tm ofs2) [va; Memstate m1] = + load_eval (OLoadRRO n2 tm ofs2) [va; Memstate m0]. +Proof. + intros until m1. + intros DISJOINT SMALL1 SMALL2 STORE0. + destruct vs as [v | ]; simpl in STORE0; try congruence. + destruct va as [base | ]; try congruence. + unfold exec_store_deps_offset in *. + unfold eval_offset in *; simpl in *. + unfold exec_load_deps_offset. + unfold Mem.storev, Mem.loadv in *. + destruct Ge in *. + unfold eval_offset in *. + unfold Val.offset_ptr in *. + destruct base as [ | | | | | wblock wpofs] in * ; try congruence. + destruct (Mem.store _ _ _ _) eqn:E0 in STORE0; try congruence. + inv STORE0. + assert ( + (Mem.load (load_chunk n2) m1 wblock + (Ptrofs.unsigned (Ptrofs.add wpofs ofs2))) = + (Mem.load (load_chunk n2) m0 wblock + (Ptrofs.unsigned (Ptrofs.add wpofs ofs2))) ) as LOADS. + { + eapply Mem.load_store_other. + eassumption. + right. + pose proof (size_chunk_positive (store_chunk n1)). + pose proof (size_chunk_positive (load_chunk n2)). + pose proof (size_chunk_small (store_chunk n1)). + pose proof (size_chunk_small (load_chunk n2)). + destruct (Intv.range_disjoint _ _ DISJOINT) as [DIS | [DIS | DIS]]; + unfold Intv.empty in DIS; simpl in DIS. + 1,2: lia. + + pose proof (Ptrofs.unsigned_range ofs1). + pose proof (Ptrofs.unsigned_range ofs2). + unfold small_offset_threshold in *. + destruct (Ptrofs.unsigned_add_either wpofs ofs1) as [R1 | R1]; rewrite R1; + destruct (Ptrofs.unsigned_add_either wpofs ofs2) as [R2 | R2]; rewrite R2; + change Ptrofs.modulus with 18446744073709551616 in *; + lia. + } + destruct (Mem.load _ m1 _ _) in *; destruct (Mem.load _ m0 _ _) in *; congruence. +Qed. + Definition goto_label_deps (f: function) (lbl: label) (vpc: val) := match label_pos lbl 0 (fn_blocks f) with | None => None -- cgit From 27767971a256b97ee75deab19a01d575ee01a6e0 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 9 Jan 2020 15:38:45 +0100 Subject: Fixing issue with "destruct ... in ..." tactics with Coq 8.8 --- mppa_k1c/Asmblockdeps.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 2cdf9499..584f2339 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -257,13 +257,13 @@ Proof. unfold Mem.storev in *. unfold Val.offset_ptr in *. destruct base as [ | | | | | wblock wpofs] in * ; try congruence. - destruct (Mem.store _ _ _ _) eqn:E0 in STORE0; try congruence. + destruct (Mem.store _ _ _ _ _) eqn:E0; try congruence. inv STORE0. - destruct (Mem.store _ _ _ _) eqn:E1 in STORE1; try congruence. + destruct (Mem.store (store_chunk n2) _ _ _ _) eqn:E1; try congruence. inv STORE1. - destruct (Mem.store _ _ _ _) eqn:E0' in STORE0'; try congruence. + destruct (Mem.store (store_chunk n2) m0 _ _ _) eqn:E0'; try congruence. inv STORE0'. - destruct (Mem.store _ _ _ _) eqn:E1' in STORE1'; try congruence. + destruct (Mem.store _ m1' _ _ _) eqn:E1'; try congruence. inv STORE1'. assert (Some m2 = Some m2'). 2: congruence. @@ -310,7 +310,7 @@ Proof. unfold eval_offset in *. unfold Val.offset_ptr in *. destruct base as [ | | | | | wblock wpofs] in * ; try congruence. - destruct (Mem.store _ _ _ _) eqn:E0 in STORE0; try congruence. + destruct (Mem.store _ _ _ _) eqn:E0; try congruence. inv STORE0. assert ( (Mem.load (load_chunk n2) m1 wblock -- cgit