From ecd4e7a1e28f7f20c1a0c8aaebbef3217a75d28f Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 3 Apr 2019 16:59:20 +0200 Subject: Load/Store reg-reg are now proven everywhere --- mppa_k1c/Asmblockdeps.v | 122 +++++++++++++++++++++--------------------------- mppa_k1c/Asmvliw.v | 38 ++++++--------- 2 files changed, 68 insertions(+), 92 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index ac8fa6bd..a06657a8 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -127,25 +127,20 @@ Definition arith_eval (ao: arith_op) (l: list value) := | _, _ => None end. -Definition exec_load_deps (chunk: memory_chunk) (m: mem) - (v: val) (ptr: ptrofs) := - match Mem.loadv chunk m (Val.offset_ptr v ptr) with - | None => None - | Some vl => Some (Val vl) - end -. - Definition exec_load_deps_offset (chunk: memory_chunk) (m: mem) (v: val) (ofs: offset) := let (ge, fn) := Ge in match (eval_offset ge ofs) with - | OK ptr => exec_load_deps chunk m v ptr + | OK ptr => match Mem.loadv chunk m (Val.offset_ptr v ptr) with + | None => None + | Some vl => Some (Val vl) + end | _ => None end. Definition exec_load_deps_reg (chunk: memory_chunk) (m: mem) (v vo: val) := - match vo with - | Vptr _ ofs => exec_load_deps chunk m v ofs - | _ => None + match Mem.loadv chunk m (Val.addl v vo) with + | None => None + | Some vl => Some (Val vl) end. Definition load_eval (lo: load_op) (l: list value) := @@ -155,25 +150,20 @@ Definition load_eval (lo: load_op) (l: list value) := | _, _ => None end. -Definition exec_store_deps (chunk: memory_chunk) (m: mem) - (vs va: val) (ptr: ptrofs) := - match Mem.storev chunk m (Val.offset_ptr va ptr) vs with - | None => None - | Some m' => Some (Memstate m') - end -. - Definition exec_store_deps_offset (chunk: memory_chunk) (m: mem) (vs va: val) (ofs: offset) := let (ge, fn) := Ge in match (eval_offset ge ofs) with - | OK ptr => exec_store_deps chunk m vs va ptr + | OK ptr => match Mem.storev chunk m (Val.offset_ptr va ptr) vs with + | None => None + | Some m' => Some (Memstate m') + end | _ => None end. Definition exec_store_deps_reg (chunk: memory_chunk) (m: mem) (vs va vo: val) := - match vo with - | Vptr _ ofs => exec_store_deps chunk m vs va ofs - | _ => None + match Mem.storev chunk m (Val.addl va vo) vs with + | None => None + | Some m' => Some (Memstate m') end. Definition store_eval (so: store_op) (l: list value) := @@ -831,47 +821,43 @@ Proof. - simpl in H. inv H. simpl macro_run. eapply trans_arith_correct; eauto. (* Load *) - - simpl in H. admit. - (* destruct i. + - simpl in H. destruct i. (* Load Offset *) + destruct i. all: - unfold exec_load_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; unfold exec_load in H; + unfold exec_load_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv H0; eexists; split; try split; [ - simpl; rewrite EVALOFF; rewrite H; rewrite (H1 ra); unfold exec_load_deps; simpl in MEML; rewrite MEML; reflexivity + simpl; rewrite EVALOFF; rewrite H; rewrite (H1 ra); simpl in MEML; rewrite MEML; reflexivity | Simpl | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ]. (* Load Reg *) + destruct i. all: - unfold exec_load_reg in H; destruct (rs rofs) eqn:ROFS; try discriminate; unfold exec_load in H; - destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv H0; - eexists; split; try split; [ - simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); unfold exec_load_deps_reg; rewrite ROFS; - unfold exec_load_deps; simpl in MEML; rewrite MEML; reflexivity + unfold exec_load_reg in H; destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv H0; + eexists; split; try split; + [ simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); unfold exec_load_deps_reg; simpl in MEML; rewrite MEML; reflexivity | Simpl - | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ]. *) + | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ]. (* Store *) - - simpl in H. admit. - (* destruct i. + - simpl in H. destruct i. (* Store Offset *) + destruct i. all: - unfold exec_store_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; unfold exec_store in H; + unfold exec_store_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv H0; eexists; split; try split; - [ simpl; rewrite EVALOFF; rewrite H; rewrite (H1 ra); rewrite (H1 rs0); unfold exec_store_deps; simpl in MEML; rewrite MEML; reflexivity + [ simpl; rewrite EVALOFF; rewrite H; rewrite (H1 ra); rewrite (H1 rs0); simpl in MEML; rewrite MEML; reflexivity | Simpl | intros rr; destruct rr; Simpl ]. (* Store Reg *) + destruct i. all: - unfold exec_store_reg in H; destruct (rs rofs) eqn:ROFS; try discriminate; unfold exec_store in H; + unfold exec_store_reg in H; destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv H0; eexists; split; try split; - [ simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); rewrite (H1 rs0); unfold exec_store_deps_reg; rewrite ROFS; - unfold exec_store_deps; simpl in MEML; rewrite MEML; reflexivity + [ simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); rewrite (H1 rs0); unfold exec_store_deps_reg; + simpl in MEML; rewrite MEML; reflexivity | Simpl | intros rr; destruct rr; Simpl ]. - *) + (* Allocframe *) - simpl in H. destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS; try discriminate. inv H. inv H0. eexists. split; try split. @@ -896,8 +882,8 @@ Proof. - simpl in H. destruct rd eqn:rdeq; try discriminate. inv H. inv H0. eexists. split; try split. Simpl. intros rr; destruct rr; Simpl. (* Pnop *) - - simpl in H. inv H. inv H0. eexists. split; try split. assumption. assumption. -Admitted. + - simpl in H. inv H. inv H0. eexists. split; try split. assumption. assumption. +Qed. Lemma forward_simu_body: forall bdy ge rs m rs' m' fn s, @@ -1213,23 +1199,23 @@ Proof. (* Load Offset *) + destruct i. all: simpl; rewrite H2; rewrite (H3 ra); unfold exec_load_offset in H0; destruct (eval_offset _ _); auto; - unfold exec_load_deps; simpl in H0; destruct (Mem.loadv _ _ _); auto; discriminate. + simpl in H0; destruct (Mem.loadv _ _ _); auto; discriminate. (* Load Reg *) - + admit. (* destruct i. all: + + destruct i. all: simpl; rewrite H2; rewrite (H3 rofs); rewrite (H3 ra); unfold exec_load_reg in H0; unfold exec_load_deps_reg; - destruct (rs rofs); auto; unfold exec_load in H0; simpl in H0; unfold exec_load_deps; destruct (Mem.loadv _ _ _); auto; discriminate. *) + destruct (rs rofs); auto; simpl in H0; destruct (Mem.loadv _ _ _); auto; discriminate. (* PStore *) - destruct i. (* Store Offset *) + destruct i. all: simpl; rewrite H2; rewrite (H3 ra); rewrite (H3 rs0); unfold exec_store_offset in H0; destruct (eval_offset _ _); auto; - simpl in H0; unfold exec_store_deps; destruct (Mem.storev _ _ _); auto; discriminate. + simpl in H0; destruct (Mem.storev _ _ _); auto; discriminate. (* Store Reg *) - + admit. (* destruct i. all: + + destruct i. all: simpl; rewrite H2; rewrite (H3 rofs); rewrite (H3 ra); rewrite (H3 rs0); simpl in H0; unfold exec_store_reg in H0; - unfold exec_store_deps_reg; destruct (rs rofs); auto; unfold exec_store in H0; unfold exec_store_deps; - destruct (Mem.storev _ _ _ _); auto; discriminate. *) + unfold exec_store_deps_reg; destruct (rs rofs); auto; + destruct (Mem.storev _ _ _ _); auto; discriminate. (* Pallocframe *) - simpl. Simpl. pose (H3 SP); simpl in e; rewrite e; clear e. rewrite H2. destruct (Mem.alloc _ _ _). simpl in H0. @@ -1243,7 +1229,7 @@ Proof. all: simpl; auto. - simpl. destruct rd; subst; try discriminate. all: simpl; auto. -Admitted. +Qed. Lemma forward_simu_body_stuck: forall bdy ge fn rs m s, @@ -1805,19 +1791,19 @@ Proof. (* Load Offset *) + destruct i; simpl load_chunk in H. all: unfold parexec_load_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; - unfold parexec_load in H; destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv MSR; inv MSW; + destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv MSR; inv MSW; eexists; split; try split; - [ simpl; rewrite EVALOFF; rewrite H; rewrite (H0 ra); unfold exec_load_deps; rewrite MEML; reflexivity + [ simpl; rewrite EVALOFF; rewrite H; rewrite (H0 ra); rewrite MEML; reflexivity | Simpl | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ]. (* Load Reg *) + destruct i; simpl load_chunk in H. all: - unfold parexec_load_reg in H; destruct (rsr rofs) eqn:ROFS; try discriminate; - unfold parexec_load in H; destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv MSR; inv MSW; + unfold parexec_load_reg in H; + destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv MSR; inv MSW; eexists; split; try split; - [ simpl; rewrite H; rewrite (H0 rofs); rewrite (H0 ra); unfold exec_load_deps_reg; rewrite ROFS; - unfold exec_load_deps; rewrite MEML; reflexivity + [ simpl; rewrite H; rewrite (H0 rofs); rewrite (H0 ra); unfold exec_load_deps_reg; + rewrite MEML; reflexivity | Simpl | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ]. @@ -1826,19 +1812,19 @@ Proof. (* Store Offset *) + destruct i; simpl store_chunk in H. all: unfold parexec_store_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; - unfold parexec_store in H; destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv MSR; inv MSW; + destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv MSR; inv MSW; eexists; split; try split; - [ simpl; rewrite EVALOFF; rewrite H; rewrite (H0 ra); rewrite (H0 rs); unfold exec_store_deps; rewrite MEML; reflexivity + [ simpl; rewrite EVALOFF; rewrite H; rewrite (H0 ra); rewrite (H0 rs); rewrite MEML; reflexivity | Simpl | intros rr; destruct rr; Simpl ]. (* Store Reg *) + destruct i; simpl store_chunk in H. all: - unfold parexec_store_reg in H; destruct (rsr rofs) eqn:ROFS; try discriminate; - unfold parexec_store in H; destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv MSR; inv MSW; + unfold parexec_store_reg in H; + destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv MSR; inv MSW; eexists; split; try split; - [ simpl; rewrite H; rewrite (H0 rofs); rewrite (H0 ra); rewrite (H0 rs); unfold exec_store_deps_reg; rewrite ROFS; - unfold exec_store_deps; rewrite MEML; reflexivity + [ simpl; rewrite H; rewrite (H0 rofs); rewrite (H0 ra); rewrite (H0 rs); unfold exec_store_deps_reg; + rewrite MEML; reflexivity | Simpl | intros rr; destruct rr; Simpl ]. @@ -1883,23 +1869,23 @@ Proof. (* Load Offset *) + destruct i; simpl in H0. all: simpl; rewrite H; rewrite (H1 ra); unfold parexec_load_offset in H0; destruct (eval_offset _ _); auto; - unfold parexec_load in H0; unfold exec_load_deps; destruct (Mem.loadv _ _ _); auto; discriminate. + destruct (Mem.loadv _ _ _); auto; discriminate. (* Load Reg *) + destruct i; simpl in H0. all: simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); unfold parexec_load_reg in H0; unfold exec_load_deps_reg; - destruct (rsr rofs); auto; unfold parexec_load in H0; unfold exec_load_deps; destruct (Mem.loadv _ _ _); auto; discriminate. + destruct (rsr rofs); auto; destruct (Mem.loadv _ _ _); auto; discriminate. (* PStore *) - destruct i. (* Store Offset *) + destruct i; simpl in H0. all: simpl; rewrite H; rewrite (H1 ra); rewrite (H1 rs); unfold parexec_store_offset in H0; destruct (eval_offset _ _); auto; - unfold parexec_store in H0; unfold exec_store_deps; destruct (Mem.storev _ _ _ _); auto; discriminate. + destruct (Mem.storev _ _ _ _); auto; discriminate. (* Store Reg *) + destruct i; simpl in H0. all: simpl; rewrite H; rewrite (H1 ra); rewrite (H1 rs); rewrite (H1 rofs); unfold parexec_store_reg in H0; unfold exec_store_deps_reg; - destruct (rsr rofs); auto; unfold parexec_store in H0; unfold exec_store_deps; destruct (Mem.storev _ _ _ _); auto; discriminate. + destruct (rsr rofs); auto; destruct (Mem.storev _ _ _ _); auto; discriminate. (* Pallocframe *) - simpl. Simpl. rewrite (H1 SP). rewrite H. destruct (Mem.alloc _ _ _). simpl in H0. destruct (Mem.store _ _ _ _); try discriminate. reflexivity. diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index cae79287..956b860b 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -69,44 +69,34 @@ Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset := (** * load/store *) (* TODO: factoriser ? *) -Definition parexec_load (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) - (d: ireg) (a: ireg) (ptr: ptrofs) := - match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with - | None => Stuck - | Some v => Next (rsw#d <- v) mw - end -. - Definition parexec_load_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a: ireg) (ofs: offset) := match (eval_offset ge ofs) with - | OK ptr => parexec_load chunk rsr rsw mr mw d a ptr + | OK ptr => match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with + | None => Stuck + | Some v => Next (rsw#d <- v) mw + end | _ => Stuck end. Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) := - match (rsr ro) with - | Vptr _ ofs => parexec_load chunk rsr rsw mr mw d a ofs - | _ => Stuck - end. - -Definition parexec_store (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) - (s: ireg) (a: ireg) (ptr: ptrofs) := - match Mem.storev chunk mr (Val.offset_ptr (rsr a) ptr) (rsr s) with + match Mem.loadv chunk mr (Val.addl (rsr a) (rsr ro)) with | None => Stuck - | Some m' => Next rsw m' - end -. + | Some v => Next (rsw#d <- v) mw + end. Definition parexec_store_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a: ireg) (ofs: offset) := match (eval_offset ge ofs) with - | OK ptr => parexec_store chunk rsr rsw mr mw s a ptr + | OK ptr => match Mem.storev chunk mr (Val.offset_ptr (rsr a) ptr) (rsr s) with + | None => Stuck + | Some m' => Next rsw m' + end | _ => Stuck end. Definition parexec_store_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a ro: ireg) := - match (rsr ro) with - | Vptr _ ofs => parexec_store chunk rsr rsw mr mw s a ofs - | _ => Stuck + match Mem.storev chunk mr (Val.addl (rsr a) (rsr ro)) (rsr s) with + | None => Stuck + | Some m' => Next rsw m' end. (* rem: parexec_store = exec_store *) -- cgit