diff options
| -rw-r--r-- | mppa_k1c/Asm.v | 16 | ||||
| -rw-r--r-- | mppa_k1c/Asmgen.v | 27 | ||||
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 7 | ||||
| -rw-r--r-- | mppa_k1c/Asmgenproof1.v | 111 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 2 |
5 files changed, 140 insertions, 23 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 72bbff69..bc8c07e4 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -226,6 +226,7 @@ Inductive instruction : Type := (* Conditional branches *) | Pcb (bt: btest) (r: ireg) (l: label) (**r branch based on btest *) + | Pcbu (bt: btest) (r: ireg) (l: label) (**r branch based on btest with unsigned semantics *) | Plb (rd: ireg) (ra: ireg) (ofs: offset) (**r load byte *) | Plbu (rd: ireg) (ra: ireg) (ofs: offset) (**r load byte unsigned *) @@ -646,6 +647,15 @@ Definition cmp_for_btest (bt: btest) := | BTdgtz => (Some Cgt, Long) end. +Definition cmpu_for_btest (bt: btest) := + match bt with + | BTwnez => (Some Cne, Int) + | BTweqz => (Some Ceq, Int) + | BTdnez => (Some Cne, Long) + | BTdeqz => (Some Ceq, Long) + | _ => (None, Int) + end. + (** Comparing integers *) Definition compare_int (t: itest) (v1 v2: val) (m: mem): val := match t with @@ -796,6 +806,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | (Some c, Long) => eval_branch f l rs m (Val.cmpl_bool c rs###r (Vlong (Int64.repr 0))) | (None, _) => Stuck 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))) + | (None, _) => Stuck + end (* (** Conditional branches, 32-bit comparisons *) | Pbeqw s1 s2 l => diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 3984c43f..0f0d3e41 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -152,13 +152,34 @@ Definition select_comp (n: int) (c: comparison) : option comparison := Definition transl_opt_compuimm (n: int) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction := match select_comp n c with - | Some Ceq => Pcb BTweqz r1 lbl :: k - | Some Cne => Pcb BTwnez r1 lbl :: k + | Some Ceq => Pcbu BTweqz r1 lbl :: k + | Some Cne => Pcbu BTwnez r1 lbl :: k | Some _ => nil (* Never happens *) | None => loadimm32 RTMP n (transl_comp c Unsigned r1 RTMP lbl k) end . +Definition select_compl (n: int64) (c: comparison) : option comparison := + if Int64.eq n Int64.zero then + match c with + | Ceq => Some Ceq + | Cne => Some Cne + | _ => None + end + else + None + . + +Definition transl_opt_compluimm + (n: int64) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction := + match select_compl n c with + | Some Ceq => Pcbu BTdeqz r1 lbl :: k + | Some Cne => Pcbu BTdnez r1 lbl :: k + | Some _ => nil (* Never happens *) + | None => loadimm64 RTMP n (transl_compl c Unsigned r1 RTMP lbl k) + end + . + Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) : res (list instruction ) := match cond, args with @@ -180,7 +201,7 @@ Definition transl_cbranch ) | Ccompluimm c n, a1 :: nil => do r1 <- ireg_of a1; - OK (loadimm64 RTMP n (transl_compl c Unsigned r1 RTMP lbl k)) + OK (transl_opt_compluimm n c r1 lbl k) | Ccompl c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (transl_compl c Signed r1 r2 lbl k) diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 905bb85c..60616311 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -209,7 +209,12 @@ Proof. - destruct (Int64.eq n Int64.zero); TailNoLabel. unfold loadimm64. destruct (make_immed64 n); TailNoLabel. unfold transl_compl; TailNoLabel. (* Ccompluimm *) - - unfold loadimm64. destruct (make_immed64 n); TailNoLabel. unfold transl_compl; TailNoLabel. + - unfold transl_opt_compluimm. + remember (select_compl n c0) as selcomp; destruct selcomp. + + destruct c; TailNoLabel; contradict Heqselcomp; unfold select_compl; + destruct (Int64.eq n Int64.zero); destruct c0; discriminate. + + unfold loadimm64; + destruct (make_immed64 n); TailNoLabel; unfold transl_compl; TailNoLabel. Qed. (* diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v index ef70cec4..62c3bb49 100644 --- a/mppa_k1c/Asmgenproof1.v +++ b/mppa_k1c/Asmgenproof1.v @@ -474,14 +474,15 @@ Proof. intros; contradict H; discriminate. } - exists rs, (Pcb BTweqz r1 lbl). + exists rs, (Pcbu BTweqz r1 lbl). split. * constructor. * split; auto. simpl. intros. - assert (Val.cmp_bool Ceq (rs r1) (Vint (Int.repr 0)) = Some b) as EVAL'S. - { rewrite <- H2. rewrite <- H0. rewrite <- H1. auto. } + (*assert (Val.cmp_bool Ceq (rs r1) (Vint (Int.repr 0)) = Some b) as EVAL'S. + { rewrite <- H2. rewrite <- H0. rewrite <- H1. auto. }*) auto; - unfold eval_branch. unfold getw. rewrite EVAL'S; auto. + unfold eval_branch. unfold getw. rewrite H0 in H2. unfold getw in H2. + rewrite H1. rewrite H2; auto. - (* c = Cne *) assert (Int.eq n Int.zero = true) as H'. { remember (Int.eq n Int.zero) as termz. destruct termz; auto. @@ -497,14 +498,12 @@ Proof. rewrite H'; simpl; auto; intros; contradict H; discriminate. } - exists rs, (Pcb BTwnez r1 lbl). + exists rs, (Pcbu BTwnez r1 lbl). split. * constructor. * split; auto. simpl. intros. - assert (Val.cmp_bool Cne (rs r1) (Vint (Int.repr 0)) = Some b) as EVAL'S. - { rewrite <- H2. rewrite <- H0. rewrite <- H1. auto. } auto; - unfold eval_branch. unfold getw. rewrite EVAL'S; auto. + unfold eval_branch. rewrite <- H0. rewrite H1. rewrite H2. auto. - (* c = Clt *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero); destruct cmp; discriminate. - (* c = Cle *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero); @@ -515,6 +514,73 @@ Proof. destruct cmp; discriminate. Qed. +Lemma transl_opt_compluimm_correct: + forall n cmp r1 lbl k rs m b c, + select_compl n cmp = Some c -> + exists rs', exists insn, + exec_straight_opt (transl_opt_compluimm n cmp r1 lbl k) rs m (insn :: 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 -> + exec_instr ge fn insn rs' m = eval_branch fn lbl rs' m (Some b)) + . +Proof. + intros. + unfold transl_opt_compluimm; rewrite H; simpl. + remember c as c'. + destruct c'. + - (* c = Ceq *) + assert (Int64.eq n Int64.zero = true) as H'. + { remember (Int64.eq n Int64.zero) as termz. destruct termz; auto. + generalize H. unfold select_compl; rewrite <- Heqtermz; simpl. + discriminate. } + assert (n = (Int64.repr 0)) as H0. { + destruct (Int64.eq_dec n (Int64.repr 0)) as [Ha|Ha]; auto. + generalize (Int64.eq_false _ _ Ha). unfold Int64.zero in H'. + rewrite H'. discriminate. + } + assert (Ceq = cmp). { + remember cmp as c0'. destruct c0'; auto; generalize H; unfold select_compl; + rewrite H'; simpl; auto; + intros; contradict H; discriminate. + } + + exists rs, (Pcbu BTdeqz r1 lbl). + split. + * constructor. + * split; auto. simpl. intros. + auto; + unfold eval_branch. rewrite H1. rewrite <- H0. destruct b; rewrite H2; auto. + - (* c = Cne *) + assert (Int64.eq n Int64.zero = true) as H'. + { remember (Int64.eq n Int64.zero) as termz. destruct termz; auto. + generalize H. unfold select_compl; rewrite <- Heqtermz; simpl. + discriminate. } + assert (n = (Int64.repr 0)) as H0. { + destruct (Int64.eq_dec n (Int64.repr 0)) as [Ha|Ha]; auto. + generalize (Int64.eq_false _ _ Ha). unfold Int64.zero in H'. + rewrite H'. discriminate. + } + assert (Cne = cmp). { + remember cmp as c0'. destruct c0'; auto; generalize H; unfold select_compl; + rewrite H'; simpl; auto; + intros; contradict H; discriminate. + } + exists rs, (Pcbu BTdnez r1 lbl). + split. + * constructor. + * split; auto. simpl. intros. + auto; + unfold eval_branch. rewrite H1. rewrite <- H0. destruct b; rewrite H2; auto. + - (* c = Clt *) contradict H; unfold select_compl; destruct (Int64.eq n Int64.zero); + destruct cmp; discriminate. + - (* c = Cle *) contradict H; unfold select_compl; destruct (Int64.eq n Int64.zero); + destruct cmp; discriminate. + - (* c = Cgt *) contradict H; unfold select_compl; destruct (Int64.eq n Int64.zero); + destruct cmp; discriminate. + - (* c = Cge *) contradict H; unfold select_compl; destruct (Int64.eq n Int64.zero); + destruct cmp; discriminate. +Qed. + Lemma transl_cbranch_correct_1: forall cond args lbl k c m ms b sp rs m', transl_cbranch cond args lbl k = OK c -> @@ -626,16 +692,25 @@ Proof. { intros. rewrite B'; eauto with asmgen. } (* Ccompluimm *) -- exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C). - exploit (transl_complu_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C'). - exists rs'2, (Pcb BTwnez GPR31 lbl). - split. - + constructor. apply exec_straight_trans - with (c2 := (transl_compl c0 Unsigned x GPR31 lbl k)) (rs2 := rs') (m2 := m'). - eexact A. eexact A'. - + split; auto. - * apply C'; auto. unfold getl. rewrite B, C; eauto with asmgen. - * intros. rewrite B'; eauto with asmgen. +- remember (select_compl n c0) as selcomp. + destruct selcomp. + + exploit (transl_opt_compluimm_correct n c0 x lbl k). apply eq_sym. apply Heqselcomp. + intros (rs' & i & A & B & C). + exists rs', i. + split. + * apply A. + * split; auto. apply C. apply EVAL'. + + unfold transl_opt_compluimm. rewrite <- Heqselcomp; simpl. + exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C). + exploit (transl_complu_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C'). + exists rs'2, (Pcb BTwnez GPR31 lbl). + split. + * constructor. apply exec_straight_trans + with (c2 := (transl_compl c0 Unsigned x GPR31 lbl k)) (rs2 := rs') (m2 := m'). + eexact A. eexact A'. + * split; auto. + { apply C'; auto. unfold getl. rewrite B, C; eauto with asmgen. } + { intros. rewrite B'; eauto with asmgen. } Qed. Lemma transl_cbranch_correct_true: diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index ca26dbbe..af7b7b30 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -252,7 +252,7 @@ module Target : TARGET = fprintf oc " compw.%a %a = %a, %a\n;;\n" icond it ireg rd ireg rs1 ireg rs2 | Pcompd (it, rd, rs1, rs2) -> fprintf oc " compd.%a %a = %a, %a\n;;\n" icond it ireg rd ireg rs1 ireg rs2 - | Pcb (bt, r, lbl) -> + | Pcb (bt, r, lbl) | Pcbu (bt, r, lbl) -> fprintf oc " cb.%a %a?%a\n;;\n" bcond bt ireg r print_label lbl | Plb(rd, ra, ofs) -> |