From d72fcc2c96f665d0c7608797b1707f2d19daa892 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 4 Apr 2018 16:01:32 +0200 Subject: MPPA - Long comparisons --- mppa_k1c/Asm.v | 29 ++++++++++- mppa_k1c/Asmgen.v | 20 ++++--- mppa_k1c/Asmgenproof.v | 8 +++ mppa_k1c/Asmgenproof1.v | 129 ++++++++++++++++++++++++++++++++++++++-------- mppa_k1c/TargetPrinter.ml | 2 + 5 files changed, 158 insertions(+), 30 deletions(-) diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index d769062f..d19f9340 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -187,6 +187,7 @@ Inductive instruction : Type := (** Comparisons *) | Pcompw (it: itest) (rd rs1 rs2: ireg) (**r integer comparison *) + | Pcompd (it: itest) (rd rs1 rs2: ireg) (**r integer comparison *) (** 32-bit integer register-immediate instructions *) | Paddiw (rd: ireg) (rs: ireg) (imm: int) (**r add immediate *) @@ -602,6 +603,31 @@ Definition compare_int (t: itest) (v1 v2: val) (m: mem): val := | ITnone => Vundef end. +Definition compare_long (t: itest) (v1 v2: val) (m: mem): val := + let res := match t with + | ITne => Val.cmpl Cne v1 v2 + | ITeq => Val.cmpl Ceq v1 v2 + | ITlt => Val.cmpl Clt v1 v2 + | ITge => Val.cmpl Cge v1 v2 + | ITle => Val.cmpl Cle v1 v2 + | ITgt => Val.cmpl Cgt v1 v2 + | ITneu => Val.cmplu (Mem.valid_pointer m) Cne v1 v2 + | ITequ => Val.cmplu (Mem.valid_pointer m) Ceq v1 v2 + | ITltu => Val.cmplu (Mem.valid_pointer m) Clt v1 v2 + | ITgeu => Val.cmplu (Mem.valid_pointer m) Cge v1 v2 + | ITleu => Val.cmplu (Mem.valid_pointer m) Cle v1 v2 + | ITgtu => Val.cmplu (Mem.valid_pointer m) Cgt v1 v2 + | ITall + | ITnall + | ITany + | ITnone => Some Vundef + end in + match res with + | Some v => v + | None => Vundef + end + . + (** Execution of a single instruction [i] in initial state [rs] and [m]. Return updated state. For instructions that correspond to actual RISC-V instructions, the cases are straightforward @@ -637,8 +663,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** Comparisons *) | Pcompw c d s1 s2 => - (* Next (nextinstr (rs#d <- (Val.cmp Cne rs##s1 rs##s2))) m *) Next (nextinstr (rs#d <- (compare_int c rs##s1 rs##s2 m))) m + | Pcompd c d s1 s2 => + Next (nextinstr (rs#d <- (compare_long c rs###s1 rs###s2 m))) m (** 32-bit integer register-immediate instructions *) | Paddiw d s i => diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index f1ff363d..710bb32c 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -128,6 +128,10 @@ Definition transl_comp (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction := Pcompw (itest_for_cmp c s) RTMP r1 r2 :: Pcb BTwnez RTMP lbl :: k. +Definition transl_compl + (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction := + Pcompd (itest_for_cmp c s) RTMP r1 r2 :: Pcb BTwnez RTMP lbl :: k. + Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) : res (list instruction ) := match cond, args with @@ -143,19 +147,19 @@ Definition transl_cbranch | Ccompimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (loadimm32 RTMP n (transl_comp c Signed r1 RTMP lbl k)) -(*| Ccompl c, a1 :: a2 :: nil => + | Ccompluimm c n, a1 :: nil => + do r1 <- ireg_of a1; + OK (loadimm64 RTMP n (transl_compl c Unsigned r1 RTMP lbl k)) + | Ccompl c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cond_int64s c rd r1 r2 k) + OK (transl_compl c Signed r1 r2 lbl k) | Ccomplu c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cond_int64u c rd r1 r2 k) + OK (transl_compl c Unsigned r1 r2 lbl k) | Ccomplimm c n, a1 :: nil => do r1 <- ireg_of a1; - OK (transl_condimm_int64s c rd r1 n k) - | Ccompluimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (transl_condimm_int64u c rd r1 n k) - | Ccompf c, f1 :: f2 :: nil => + OK (loadimm64 RTMP n (transl_compl c Signed r1 RTMP lbl k)) +(*| Ccompf c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; let (insn, normal) := transl_cond_float c rd r1 r2 in OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k) diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 1e616a01..3dce24cf 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -188,6 +188,14 @@ Proof. - unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel. (* Ccompuimm *) - unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel. +(* Ccompl *) + - unfold transl_compl; TailNoLabel. +(* Ccomplu *) + - unfold transl_compl; TailNoLabel. +(* Ccomplimm *) + - unfold loadimm64. destruct (make_immed64 n); TailNoLabel. unfold transl_compl; TailNoLabel. +(* Ccompluimm *) + - 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 e83ef307..fe037994 100644 --- a/mppa_k1c/Asmgenproof1.v +++ b/mppa_k1c/Asmgenproof1.v @@ -144,6 +144,22 @@ Proof. split. Simpl. intros; Simpl. Qed. + +Lemma loadimm64_correct: + forall rd n k rs m, + exists rs', + exec_straight ge fn (loadimm64 rd n k) rs m k rs' m + /\ rs'#rd = Vlong n + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. +Proof. + unfold loadimm64; intros. generalize (make_immed64_sound n); intros E. + destruct (make_immed64 n). +- subst imm. econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. + intros; Simpl. +Qed. + (* Lemma opimm32_correct: forall (op: ireg -> ireg0 -> ireg0 -> instruction) @@ -194,28 +210,8 @@ Proof. split. Simpl. intros; Simpl. Qed. - -Lemma loadimm64_correct: - forall rd n k rs m, - exists rs', - exec_straight ge fn (loadimm64 rd n k) rs m k rs' m - /\ rs'#rd = Vlong n - /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. -Proof. - unfold loadimm64; intros. generalize (make_immed64_sound n); intros E. - destruct (make_immed64 n). -- subst imm. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. rewrite Int64.add_zero_l; Simpl. - intros; Simpl. -- exploit load_hilo64_correct; eauto. intros (rs' & A & B & C). - rewrite E. exists rs'; eauto. -- subst imm. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -Qed. *) + Lemma opimm64_correct: forall (op: ireg -> ireg -> ireg -> instruction) (opi: ireg -> ireg -> int64 -> instruction) @@ -390,6 +386,63 @@ Proof. rewrite H0. simpl; auto. Qed. +Lemma transl_compl_correct: + forall cmp r1 r2 lbl k rs m b, + exists rs', + exec_straight ge fn (transl_compl cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl :: k) rs' m + /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) + /\ ( Val.cmpl_bool cmp rs###r1 rs###r2 = Some b -> + exec_instr ge fn (Pcb BTwnez GPR31 lbl) rs' m = eval_branch fn lbl rs' m (Some b)) + . +Proof. + intros. esplit. split. +- unfold transl_compl. apply exec_straight_one; simpl; eauto. +- split. + + intros; Simpl. + + intros. + remember (nextinstr rs # GPR31 <- (compare_long (itest_for_cmp cmp Signed) rs ### r1 rs ### r2 m)) as rs'. + simpl. assert (Val.cmp_bool Cne rs' ## GPR31 (Vint (Int.repr 0)) = Some b). + { + assert (rs' ## GPR31 = (compare_long (itest_for_cmp cmp Signed) rs ### r1 rs ### r2 m)). + { rewrite Heqrs'. auto. } + rewrite H0. rewrite <- H. + remember (Val.cmpl_bool cmp rs###r1 rs###r2) as cmpbool. + destruct cmp; simpl; + unfold compare_long; + unfold Val.cmpl; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; + destruct b0; simpl; auto. + } + rewrite H0. simpl; auto. +Qed. + +Lemma transl_complu_correct: + forall cmp r1 r2 lbl k rs m b, + exists rs', + exec_straight ge fn (transl_compl cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl :: k) rs' m + /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) + /\ ( Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2 = Some b -> + exec_instr ge fn (Pcb BTwnez GPR31 lbl) rs' m = eval_branch fn lbl rs' m (Some b)) + . +Proof. + intros. esplit. split. +- unfold transl_compl. apply exec_straight_one; simpl; eauto. +- split. + + intros; Simpl. + + intros. + remember (nextinstr rs # GPR31 <- (compare_long (itest_for_cmp cmp Unsigned) rs ### r1 rs ### r2 m)) as rs'. + simpl. assert (Val.cmp_bool Cne rs' ## GPR31 (Vint (Int.repr 0)) = Some b). + { + assert (rs' ## GPR31 = (compare_long (itest_for_cmp cmp Unsigned) rs ### r1 rs ### r2 m)). + { rewrite Heqrs'. auto. } + rewrite H0. rewrite <- H. + remember (Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2) as cmpbool. + destruct cmp; simpl; + unfold compare_long; + unfold Val.cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; + destruct b0; simpl; auto. + } + rewrite H0. simpl; auto. +Qed. Lemma transl_cbranch_correct_1: forall cond args lbl k c m ms b sp rs m', @@ -442,6 +495,40 @@ Proof. + split; auto. * apply C'; auto. unfold getw. rewrite B, C; eauto with asmgen. * intros. rewrite B'; eauto with asmgen. +(* Ccompl *) +- exploit (transl_compl_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C). + exists rs', (Pcb BTwnez GPR31 lbl). + split. + + constructor. eexact A. + + split; auto. apply C; auto. +(* Ccomplu *) +- exploit (transl_complu_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C). + exists rs', (Pcb BTwnez GPR31 lbl). + split. + + constructor. eexact A. + + split; auto. apply C; auto. +(* Ccomplimm *) +- exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C). + exploit (transl_compl_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 Signed 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. +(* 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. Qed. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 2c7b8cc8..2fafb127 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -210,6 +210,8 @@ module Target : TARGET = | Pcompw (it, rd, rs1, rs2) -> 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) -> fprintf oc " cb.%a %a?%a\n;;\n" bcond bt ireg r print_label lbl -- cgit