From 6bff68d55932bdc4715741a973724317c639b833 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Mar 2021 12:13:19 +0100 Subject: Merge conflicts solved and cleaning in Asmgenproof after expansion --- riscV/Asmgen.v | 253 --------------------------------------------------------- 1 file changed, 253 deletions(-) (limited to 'riscV/Asmgen.v') diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 252a9270..957166b6 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -105,8 +105,6 @@ Definition addimm32 := opimm32 Paddw Paddiw. Definition andimm32 := opimm32 Pandw Pandiw. Definition orimm32 := opimm32 Porw Poriw. Definition xorimm32 := opimm32 Pxorw Pxoriw. -Definition sltimm32 := opimm32 Psltw Psltiw. -Definition sltuimm32 := opimm32 Psltuw Psltiuw. Definition load_hilo64 (r: ireg) (hi lo: int64) k := if Int64.eq lo Int64.zero then Pluil r hi :: k @@ -132,8 +130,6 @@ Definition addimm64 := opimm64 Paddl Paddil. Definition andimm64 := opimm64 Pandl Pandil. Definition orimm64 := opimm64 Porl Poril. Definition xorimm64 := opimm64 Pxorl Pxoril. -Definition sltimm64 := opimm64 Psltl Psltil. -Definition sltuimm64 := opimm64 Psltul Psltiul. Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) := if Ptrofs.eq_dec n Ptrofs.zero then @@ -145,66 +141,6 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) := (** Translation of conditional branches. *) -Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) := - match cmp with - | Ceq => Pbeqw r1 r2 lbl - | Cne => Pbnew r1 r2 lbl - | Clt => Pbltw r1 r2 lbl - | Cle => Pbgew r2 r1 lbl - | Cgt => Pbltw r2 r1 lbl - | Cge => Pbgew r1 r2 lbl - end. - -Definition transl_cbranch_int32u (cmp: comparison) (r1 r2: ireg0) (lbl: label) := - match cmp with - | Ceq => Pbeqw r1 r2 lbl - | Cne => Pbnew r1 r2 lbl - | Clt => Pbltuw r1 r2 lbl - | Cle => Pbgeuw r2 r1 lbl - | Cgt => Pbltuw r2 r1 lbl - | Cge => Pbgeuw r1 r2 lbl - end. - -Definition transl_cbranch_int64s (cmp: comparison) (r1 r2: ireg0) (lbl: label) := - match cmp with - | Ceq => Pbeql r1 r2 lbl - | Cne => Pbnel r1 r2 lbl - | Clt => Pbltl r1 r2 lbl - | Cle => Pbgel r2 r1 lbl - | Cgt => Pbltl r2 r1 lbl - | Cge => Pbgel r1 r2 lbl - end. - -Definition transl_cbranch_int64u (cmp: comparison) (r1 r2: ireg0) (lbl: label) := - match cmp with - | Ceq => Pbeql r1 r2 lbl - | Cne => Pbnel r1 r2 lbl - | Clt => Pbltul r1 r2 lbl - | Cle => Pbgeul r2 r1 lbl - | Cgt => Pbltul r2 r1 lbl - | Cge => Pbgeul r1 r2 lbl - end. - -Definition transl_cond_float (cmp: comparison) (rd: ireg) (fs1 fs2: freg) := - match cmp with - | Ceq => (Pfeqd rd fs1 fs2, true) - | Cne => (Pfeqd rd fs1 fs2, false) - | Clt => (Pfltd rd fs1 fs2, true) - | Cle => (Pfled rd fs1 fs2, true) - | Cgt => (Pfltd rd fs2 fs1, true) - | Cge => (Pfled rd fs2 fs1, true) - end. - -Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) := - match cmp with - | Ceq => (Pfeqs rd fs1 fs2, true) - | Cne => (Pfeqs rd fs1 fs2, false) - | Clt => (Pflts rd fs1 fs2, true) - | Cle => (Pfles rd fs1 fs2, true) - | Cgt => (Pflts rd fs2 fs1, true) - | Cge => (Pfles rd fs2 fs1, true) - end. - Definition apply_bin_r0_r0r0lbl (optR0: option bool) (sem: ireg0 -> ireg0 -> label -> instruction) (r1 r2: ireg0) (lbl: label) := match optR0 with | None => sem r1 r2 lbl @@ -222,59 +158,6 @@ Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instru Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) := match cond, args with - | Ccomp c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cbranch_int32s c r1 r2 lbl :: k) - | Ccompu c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cbranch_int32u c r1 r2 lbl :: k) - | Ccompimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (if Int.eq n Int.zero then - transl_cbranch_int32s c r1 X0 lbl :: k - else - loadimm32 X31 n (transl_cbranch_int32s c r1 X31 lbl :: k)) - | Ccompuimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (if Int.eq n Int.zero then - transl_cbranch_int32u c r1 X0 lbl :: k - else - loadimm32 X31 n (transl_cbranch_int32u c r1 X31 lbl :: k)) - | Ccompl c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cbranch_int64s c r1 r2 lbl :: k) - | Ccomplu c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cbranch_int64u c r1 r2 lbl :: k) - | Ccomplimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (if Int64.eq n Int64.zero then - transl_cbranch_int64s c r1 X0 lbl :: k - else - loadimm64 X31 n (transl_cbranch_int64s c r1 X31 lbl :: k)) - | Ccompluimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (if Int64.eq n Int64.zero then - transl_cbranch_int64u c r1 X0 lbl :: k - else - loadimm64 X31 n (transl_cbranch_int64u c r1 X31 lbl :: k)) - | Ccompf c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c X31 r1 r2 in - OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k) - | Cnotcompf c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c X31 r1 r2 in - OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k) - | Ccompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c X31 r1 r2 in - OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k) - | Cnotcompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c X31 r1 r2 in - OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k) - | CEbeqw optR0, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (apply_bin_r0_r0r0lbl optR0 Pbeqw r1 r2 lbl :: k) @@ -327,133 +210,6 @@ Definition transl_cbranch Error(msg "Asmgen.transl_cond_branch") end. -(** Translation of a condition operator. The generated code sets the - [rd] target register to 0 or 1 depending on the truth value of the - condition. *) - -Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) := - match cmp with - | Ceq => Pseqw rd r1 r2 :: k - | Cne => Psnew rd r1 r2 :: k - | Clt => Psltw rd r1 r2 :: k - | Cle => Psltw rd r2 r1 :: Pxoriw rd rd Int.one :: k - | Cgt => Psltw rd r2 r1 :: k - | Cge => Psltw rd r1 r2 :: Pxoriw rd rd Int.one :: k - end. - -Definition transl_cond_int32u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) := - match cmp with - | Ceq => Pseqw rd r1 r2 :: k - | Cne => Psnew rd r1 r2 :: k - | Clt => Psltuw rd r1 r2 :: k - | Cle => Psltuw rd r2 r1 :: Pxoriw rd rd Int.one :: k - | Cgt => Psltuw rd r2 r1 :: k - | Cge => Psltuw rd r1 r2 :: Pxoriw rd rd Int.one :: k - end. - -Definition transl_cond_int64s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) := - match cmp with - | Ceq => Pseql rd r1 r2 :: k - | Cne => Psnel rd r1 r2 :: k - | Clt => Psltl rd r1 r2 :: k - | Cle => Psltl rd r2 r1 :: Pxoriw rd rd Int.one :: k - | Cgt => Psltl rd r2 r1 :: k - | Cge => Psltl rd r1 r2 :: Pxoriw rd rd Int.one :: k - end. - -Definition transl_cond_int64u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) := - match cmp with - | Ceq => Pseql rd r1 r2 :: k - | Cne => Psnel rd r1 r2 :: k - | Clt => Psltul rd r1 r2 :: k - | Cle => Psltul rd r2 r1 :: Pxoriw rd rd Int.one :: k - | Cgt => Psltul rd r2 r1 :: k - | Cge => Psltul rd r1 r2 :: Pxoriw rd rd Int.one :: k - end. - -Definition transl_condimm_int32s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) := - if Int.eq n Int.zero then transl_cond_int32s cmp rd r1 X0 k else - match cmp with - | Ceq | Cne => xorimm32 rd r1 n (transl_cond_int32s cmp rd rd X0 k) - | Clt => sltimm32 rd r1 n k - | Cle => if Int.eq n (Int.repr Int.max_signed) - then loadimm32 rd Int.one k - else sltimm32 rd r1 (Int.add n Int.one) k - | _ => loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k) - end. - -Definition transl_condimm_int32u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) := - if Int.eq n Int.zero then transl_cond_int32u cmp rd r1 X0 k else - match cmp with - | Clt => sltuimm32 rd r1 n k - | _ => loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k) - end. - -Definition transl_condimm_int64s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) := - if Int64.eq n Int64.zero then transl_cond_int64s cmp rd r1 X0 k else - match cmp with - | Ceq | Cne => xorimm64 rd r1 n (transl_cond_int64s cmp rd rd X0 k) - | Clt => sltimm64 rd r1 n k - | Cle => if Int64.eq n (Int64.repr Int64.max_signed) - then loadimm32 rd Int.one k - else sltimm64 rd r1 (Int64.add n Int64.one) k - | _ => loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k) - end. - -Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) := - if Int64.eq n Int64.zero then transl_cond_int64u cmp rd r1 X0 k else - match cmp with - | Clt => sltuimm64 rd r1 n k - | _ => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k) - end. - -Definition transl_cond_op - (cond: condition) (rd: ireg) (args: list mreg) (k: code) := - match cond, args with - | Ccomp c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cond_int32s c rd r1 r2 k) - | Ccompu c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cond_int32u c rd r1 r2 k) - | Ccompimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (transl_condimm_int32s c rd r1 n k) - | Ccompuimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (transl_condimm_int32u c rd r1 n 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) - | Ccomplu c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cond_int64u c rd r1 r2 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 => - 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) - | Cnotcompf 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 Pxoriw rd rd Int.one :: k else k) - | Ccompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c rd r1 r2 in - OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k) - | Cnotcompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c rd r1 r2 in - OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) - | _, _ => - Error(msg "Asmgen.transl_cond_op") - end. - (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) @@ -767,9 +523,6 @@ Definition transl_op | Osingleoflongu, a1 :: nil => do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfcvtslu rd rs :: k) - | Ocmp cmp, _ => - do rd <- ireg_of res; - transl_cond_op cmp rd args k | OEseqw optR0, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; @@ -912,18 +665,12 @@ Definition transl_op | Ofloat_of_bits, a1 :: nil => do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfmvdx rd rs :: k) - - | Ocmp cmp, _ => - do rd <- ireg_of res; - transl_cond_op cmp rd args k - | Oselectl, b::t::f::nil => do rd <- ireg_of res; do rb <- ireg_of b; do rt <- ireg_of t; do rf <- ireg_of f; OK (Pselectl rd rb rt rf :: k) - | _, _ => Error(msg "Asmgen.transl_op") end. -- cgit