From 8f972659841ad38f6f548161b5ca3cfcbdd135cb Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 13 Mar 2019 10:53:15 +0100 Subject: Enlevé la dépendance mémoire de Pcbu MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mppa_k1c/Asmblock.v | 4 ++-- mppa_k1c/Asmblockdeps.v | 40 ++++++++++++++++++++-------------------- mppa_k1c/Asmblockgenproof1.v | 6 +++--- 3 files changed, 25 insertions(+), 25 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 9938b386..621ed8a7 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -1390,8 +1390,8 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) end | Pcbu bt r l => match cmpu_for_btest bt with - | (Some c, Int) => eval_branch f l rs m (Val.cmpu_bool (Mem.valid_pointer m) c rs#r (Vint (Int.repr 0))) - | (Some c, Long) => eval_branch f l rs m (Val.cmplu_bool (Mem.valid_pointer m) c rs#r (Vlong (Int64.repr 0))) + | (Some c, Int) => eval_branch f l rs m (Val_cmpu_bool c rs#r (Vint (Int.repr 0))) + | (Some c, Long) => eval_branch f l rs m (Val_cmplu_bool c rs#r (Vlong (Int64.repr 0))) | (None, _) => Stuck end diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 616c5f2a..c6052337 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -179,10 +179,10 @@ Definition control_eval (o: control_op) (l: list value) := | (Some c, Long) => eval_branch_deps fn l vpc (Val.cmpl_bool c v (Vlong (Int64.repr 0))) | (None, _) => None end - | Ocbu bt l, [Val v; Val vpc; Memstate m] => + | Ocbu bt l, [Val v; Val vpc] => match cmpu_for_btest bt with - | (Some c, Int) => eval_branch_deps fn l vpc (Val.cmpu_bool (Mem.valid_pointer m) c v (Vint (Int.repr 0))) - | (Some c, Long) => eval_branch_deps fn l vpc (Val.cmplu_bool (Mem.valid_pointer m) c v (Vlong (Int64.repr 0))) + | (Some c, Int) => eval_branch_deps fn l vpc (Val_cmpu_bool c v (Vint (Int.repr 0))) + | (Some c, Long) => eval_branch_deps fn l vpc (Val_cmplu_bool c v (Vlong (Int64.repr 0))) | (None, _) => None end | OIncremPC sz, [Val vpc] => Some (Val (Val.offset_ptr vpc (Ptrofs.repr sz))) @@ -503,7 +503,7 @@ Definition trans_control (ctl: control) : macro := | Pigoto r => [(#PC, Name (#r))] | Pj_l l => [(#PC, Op (Control (Oj_l l)) (Name (#PC) @ Enil))] | Pcb bt r l => [(#PC, Op (Control (Ocb bt l)) (Name (#r) @ Name (#PC) @ Enil))] - | Pcbu bt r l => [(#PC, Op (Control (Ocbu bt l)) (Name (#r) @ Name (#PC) @ Name pmem @ Enil))] + | Pcbu bt r l => [(#PC, Op (Control (Ocbu bt l)) (Name (#r) @ Name (#PC) @ Enil))] | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)] end. @@ -844,34 +844,34 @@ Proof. * intros rr; destruct rr; Simpl. (* Pcbu *) + destruct (cmpu_for_btest _) eqn:CFB. destruct o; try discriminate. destruct i. - ++ unfold eval_branch in H0. destruct (Val.cmpu_bool _ _ _) eqn:VALCMP; try discriminate. destruct b0. + ++ unfold eval_branch in H0. destruct (Val_cmpu_bool _ _) eqn:VALCMP; try discriminate. destruct b0. +++ unfold goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (nextblock b rs PC) eqn:NB; try discriminate. inv H0. eexists; split; try split. * simpl control_eval. pose (H3 PC); simpl in e; rewrite e. simpl. - rewrite CFB. Simpl. rewrite H2. pose (H3 r). simpl in e0. rewrite e0. + rewrite CFB. Simpl. pose (H3 r). simpl in e0. rewrite e0. unfold eval_branch_deps. unfold nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP. unfold goto_label_deps. rewrite LPOS. rewrite nextblock_pc in NB. rewrite NB. reflexivity. * Simpl. * intros rr; destruct rr; Simpl. +++ inv H0. eexists; split; try split. * simpl control_eval. pose (H3 PC); simpl in e; rewrite e. simpl. - rewrite CFB. Simpl. rewrite H2. pose (H3 r). simpl in e0. rewrite e0. + rewrite CFB. Simpl. pose (H3 r). simpl in e0. rewrite e0. unfold eval_branch_deps. unfold nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP. reflexivity. * Simpl. * intros rr; destruct rr; Simpl. - ++ unfold eval_branch in H0. destruct (Val.cmplu_bool _ _ _) eqn:VALCMP; try discriminate. destruct b0. + ++ unfold eval_branch in H0. destruct (Val_cmplu_bool _ _) eqn:VALCMP; try discriminate. destruct b0. +++ unfold goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (nextblock b rs PC) eqn:NB; try discriminate. inv H0. eexists; split; try split. * simpl control_eval. pose (H3 PC); simpl in e; rewrite e. simpl. - rewrite CFB. Simpl. rewrite H2. pose (H3 r). simpl in e0. rewrite e0. + rewrite CFB. Simpl. pose (H3 r). simpl in e0. rewrite e0. unfold eval_branch_deps. unfold nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP. unfold goto_label_deps. rewrite LPOS. rewrite nextblock_pc in NB. rewrite NB. reflexivity. * Simpl. * intros rr; destruct rr; Simpl. +++ inv H0. eexists; split; try split. * simpl control_eval. pose (H3 PC); simpl in e; rewrite e. simpl. - rewrite CFB. Simpl. rewrite H2. pose (H3 r). simpl in e0. rewrite e0. + rewrite CFB. Simpl. pose (H3 r). simpl in e0. rewrite e0. unfold eval_branch_deps. unfold nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP. reflexivity. * Simpl. @@ -1013,17 +1013,17 @@ Proof. (* Pcbu *) - simpl in *. destruct (cmpu_for_btest bt). destruct i. + pose (H3 PC); simpl in e; rewrite e in H1; clear e. - destruct o; auto. rewrite H2 in H1. + destruct o; auto. pose (H3 r); simpl in e; rewrite e in H1; clear e. unfold eval_branch_deps in H1; unfold eval_branch. - destruct (Val.cmpu_bool _ _ _ _); auto. destruct b; try discriminate. + destruct (Val_cmpu_bool _ _ _); auto. destruct b; try discriminate. unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. + pose (H3 PC); simpl in e; rewrite e in H1; clear e. - destruct o; auto. rewrite H2 in H1. + destruct o; auto. pose (H3 r); simpl in e; rewrite e in H1; clear e. unfold eval_branch_deps in H1; unfold eval_branch. - destruct (Val.cmplu_bool _ _ _); auto. destruct b; try discriminate. + destruct (Val_cmplu_bool _ _); auto. destruct b; try discriminate. unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. Qed. @@ -1123,17 +1123,17 @@ Proof. (* Pcbu *) - simpl in *. destruct (cmpu_for_btest bt). destruct i. -- destruct o. - + rewrite H2. unfold eval_branch in H0; unfold eval_branch_deps. - pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmpu_bool _ _ _); auto. + + unfold eval_branch in H0; unfold eval_branch_deps. + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val_cmpu_bool _ _); auto. destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0. destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. - + rewrite H2. pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity. + + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity. -- destruct o. - + rewrite H2. unfold eval_branch in H0; unfold eval_branch_deps. - pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmplu_bool _ _ _); auto. + + unfold eval_branch in H0; unfold eval_branch_deps. + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val_cmplu_bool _ _); auto. destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0. destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. - + rewrite H2. pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity. + + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity. Qed. diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 1a55f58e..5486a497 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -743,7 +743,7 @@ Lemma transl_opt_compuimm_correct: exists rs', exists insn, exec_straight_opt (transl_opt_compuimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) - /\ ( Val.cmpu_bool (Mem.valid_pointer m) cmp rs#r1 (Vint n) = Some b -> + /\ ( Val_cmpu_bool cmp rs#r1 (Vint n) = Some b -> exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b)) . Proof. @@ -819,7 +819,7 @@ Lemma transl_opt_compluimm_correct: exists rs', exists insn, exec_straight_opt (transl_opt_compluimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) - /\ ( Val.cmplu_bool (Mem.valid_pointer m) cmp rs#r1 (Vlong n) = Some b -> + /\ ( Val_cmplu_bool cmp rs#r1 (Vlong n) = Some b -> exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b)) . Proof. @@ -1016,7 +1016,7 @@ Proof. exists rs', i. split. * apply A. - * split; auto. apply C. apply EVAL'. + * split; eauto. (* apply C. apply EVAL'. *) + assert (transl_opt_compluimm n c0 x lbl k = loadimm64 RTMP n ::g transl_compl c0 Unsigned x RTMP lbl k). { unfold transl_opt_compluimm. destruct (Int64.eq n Int64.zero) eqn:EQN. -- cgit