diff options
-rw-r--r-- | extraction/debug/Asmgen.ml | 16 | ||||
-rw-r--r-- | mppa_k1c/Asm.v | 354 | ||||
-rw-r--r-- | mppa_k1c/Asmgen.v | 213 | ||||
-rw-r--r-- | mppa_k1c/Asmgenproof.v | 18 | ||||
-rw-r--r-- | mppa_k1c/Asmgenproof1.v | 254 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 363 | ||||
-rw-r--r-- | test/mppa/Makefile | 4 | ||||
-rw-r--r-- | test/mppa/branch.c | 12 |
8 files changed, 288 insertions, 946 deletions
diff --git a/extraction/debug/Asmgen.ml b/extraction/debug/Asmgen.ml index 84faf75a..2ccc5948 100644 --- a/extraction/debug/Asmgen.ml +++ b/extraction/debug/Asmgen.ml @@ -195,3 +195,19 @@ let transl_instr f i x k = | Mcond _ -> (Printf.eprintf "Mcond\n"; thereal_transl_instr f i x k) | Mjumptable _ -> (Printf.eprintf "Mjumptable\n"; thereal_transl_instr f i x k) | Mreturn -> (Printf.eprintf "Mreturn\n"; thereal_transl_instr f i x k) + +let transl_cbranch c a l k = + match c, a with + | Ccomp _, _ :: _ :: [] -> (Printf.eprintf "Ccomp\n"; thereal_transl_cbranch c a l k) + | Ccompu _, _ :: _ :: [] -> (Printf.eprintf "Ccompu\n"; thereal_transl_cbranch c a l k) + | Ccompimm (_, _), _ :: [] -> (Printf.eprintf "Ccompimm\n"; thereal_transl_cbranch c a l k) + | Ccompuimm (_, _), _ :: [] -> (Printf.eprintf "Ccompuimm\n"; thereal_transl_cbranch c a l k) + | Ccompl _, _ :: _ :: [] -> (Printf.eprintf "Ccompl\n"; thereal_transl_cbranch c a l k) + | Ccomplu _, _ :: _ :: [] -> (Printf.eprintf "Ccomplu\n"; thereal_transl_cbranch c a l k) + | Ccomplimm (_, _), _ :: [] -> (Printf.eprintf "Ccomplimm\n"; thereal_transl_cbranch c a l k) + | Ccompluimm (_, _), _ :: [] -> (Printf.eprintf "Ccompulimm\n"; thereal_transl_cbranch c a l k) + | Ccompf _, _ :: _ :: [] -> (Printf.eprintf "Ccompf\n"; thereal_transl_cbranch c a l k) + | Cnotcompf _, _ :: _ :: [] -> (Printf.eprintf "Cnotcompf\n"; thereal_transl_cbranch c a l k) + | Ccompfs _, _ :: _ :: [] -> (Printf.eprintf "Ccomps\n"; thereal_transl_cbranch c a l k) + | Cnotcompfs _, _ :: _ :: [] -> (Printf.eprintf "Cnotcomps\n"; thereal_transl_cbranch c a l k) + | _ -> (Printf.eprintf "OOPS\n"; thereal_transl_cbranch c a l k) diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 82ec101c..d769062f 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -92,6 +92,44 @@ Module Pregmap := EMap(PregEq). (** Conventional names for stack pointer ([SP]) and return address ([RA]). *) Notation "'SP'" := GPR12 (only parsing) : asm. +Notation "'RTMP'" := GPR31 (only parsing) : asm. + +Inductive btest: Type := +(*| BTdnez (**r Double Not Equal to Zero *) + | BTdeqz (**r Double Equal to Zero *) + | BTdltz (**r Double Less Than Zero *) + | BTdgez (**r Double Greater Than or Equal to Zero *) + | BTdlez (**r Double Less Than or Equal to Zero *) + | BTdgtz (**r Double Greater Than Zero *) + | BTodd (**r Odd (LSB Set) *) + | BTeven (**r Even (LSB Clear) *) +*)| BTwnez (**r Word Not Equal to Zero *) + | BTweqz (**r Word Equal to Zero *) +(*| BTwltz (**r Word Less Than Zero *) + | BTwgez (**r Word Greater Than or Equal to Zero *) + | BTwlez (**r Word Less Than or Equal to Zero *) + | BTwgtz (**r Word Greater Than Zero *) +*). + +Inductive itest: Type := + | ITne (**r Not Equal *) + | ITeq (**r Equal *) + | ITlt (**r Less Than *) + | ITge (**r Greater Than or Equal *) + | ITle (**r Less Than or Equal *) + | ITgt (**r Greater Than *) + | ITneu (**r Unsigned Not Equal *) + | ITequ (**r Unsigned Equal *) + | ITltu (**r Less Than Unsigned *) + | ITgeu (**r Greater Than or Equal Unsigned *) + | ITleu (**r Less Than or Equal Unsigned *) + | ITgtu (**r Greater Than Unsigned *) + (* Not used yet *) + | ITall (**r All Bits Set in Mask *) + | ITnall (**r Not All Bits Set in Mask *) + | ITany (**r Any Bits Set in Mask *) + | ITnone (**r Not Any Bits Set in Mask *) + . (** Offsets for load and store instructions. An offset is either an immediate integer or the low part of a symbol. *) @@ -136,121 +174,46 @@ Definition label := positive. [Asmgen]) is careful to respect this range. *) Inductive instruction : Type := +(** System Registers *) + | Pget (rd: ireg) (rs: preg) (**r get system register *) + | Pset (rd: preg) (rs: ireg) (**r set system register *) (** Branch Control Unit instructions *) - | Pget (rd: ireg) (rs: preg) (**r get system register *) - | Pset (rd: preg) (rs: ireg) (**r set system register *) - | Pret (**r return *) - | Pcall (l: label) (**r function call *) - | Pgoto (l: label) (**r goto *) - | Pmv (rd: ireg) (rs: ireg) (**r integer move *) + | Pret (**r return *) + | Pcall (l: label) (**r function call *) + | Pgoto (l: label) (**r goto *) + +(** Register move *) + | Pmv (rd: ireg) (rs: ireg) (**r integer move *) + +(** Comparisons *) + | Pcompw (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 *) -(*| Psltiw (rd: ireg) (rs: ireg) (imm: int) (**r set-less-than immediate *) - | Psltiuw (rd: ireg) (rs: ireg) (imm: int) (**r set-less-than unsigned immediate *) - | Pandiw (rd: ireg) (rs: ireg) (imm: int) (**r and immediate *) - | Poriw (rd: ireg) (rs: ireg) (imm: int) (**r or immediate *) - | Pxoriw (rd: ireg) (rs: ireg) (imm: int) (**r xor immediate *) - | Pslliw (rd: ireg) (rs: ireg) (imm: int) (**r shift-left-logical immediate *) - | Psrliw (rd: ireg) (rs: ireg) (imm: int) (**r shift-right-logical immediate *) - | Psraiw (rd: ireg) (rs: ireg) (imm: int) (**r shift-right-arith immediate *) - | Pluiw (rd: ireg) (imm: int) (**r load upper-immediate *) + (** 32-bit integer register-register instructions *) -*)| Paddw (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) -(*| Psubw (rd: ireg) (rs1 rs2: ireg) (**r integer subtraction *) - - | Pmulw (rd: ireg) (rs1 rs2: ireg) (**r integer multiply low *) - | Pmulhw (rd: ireg) (rs1 rs2: ireg) (**r integer multiply high signed *) - | Pmulhuw (rd: ireg) (rs1 rs2: ireg) (**r integer multiply high unsigned *) - | Pdivw (rd: ireg) (rs1 rs2: ireg) (**r integer division *) - | Pdivuw (rd: ireg) (rs1 rs2: ireg) (**r unsigned integer division *) - | Premw (rd: ireg) (rs1 rs2: ireg) (**r integer remainder *) - | Premuw (rd: ireg) (rs1 rs2: ireg) (**r unsigned integer remainder *) - | Psltw (rd: ireg) (rs1 rs2: ireg) (**r set-less-than *) - | Psltuw (rd: ireg) (rs1 rs2: ireg) (**r set-less-than unsigned *) - | Pseqw (rd: ireg) (rs1 rs2: ireg) (**r [rd <- rs1 == rs2] (pseudo) *) - | Psnew (rd: ireg) (rs1 rs2: ireg) (**r [rd <- rs1 != rs2] (pseudo) *) - | Pandw (rd: ireg) (rs1 rs2: ireg) (**r bitwise and *) - | Porw (rd: ireg) (rs1 rs2: ireg) (**r bitwise or *) - | Pxorw (rd: ireg) (rs1 rs2: ireg) (**r bitwise xor *) - | Psllw (rd: ireg) (rs1 rs2: ireg) (**r shift-left-logical *) - | Psrlw (rd: ireg) (rs1 rs2: ireg) (**r shift-right-logical *) - | Psraw (rd: ireg) (rs1 rs2: ireg) (**r shift-right-arith *) + | Paddw (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) (** 64-bit integer register-immediate instructions *) -*)| Paddil (rd: ireg) (rs: ireg) (imm: int64) (**r add immediate *) (* - | Psltil (rd: ireg) (rs: ireg) (imm: int64) (**r set-less-than immediate *) - | Psltiul (rd: ireg) (rs: ireg) (imm: int64) (**r set-less-than unsigned immediate *) - | Pandil (rd: ireg) (rs: ireg) (imm: int64) (**r and immediate *) - | Poril (rd: ireg) (rs: ireg) (imm: int64) (**r or immediate *) - | Pxoril (rd: ireg) (rs: ireg) (imm: int64) (**r xor immediate *) - | Psllil (rd: ireg) (rs: ireg) (imm: int) (**r shift-left-logical immediate *) - | Psrlil (rd: ireg) (rs: ireg) (imm: int) (**r shift-right-logical immediate *) - | Psrail (rd: ireg) (rs: ireg) (imm: int) (**r shift-right-arith immediate *) - | Pluil (rd: ireg) (imm: int64) (**r FIXME - remove it ; load upper-immediate *) -*)| Pmake (rd: ireg) (imm: int) (**r load immediate *) - | Pmakel (rd: ireg) (imm: int64) (**r load immediate long *) + | Paddil (rd: ireg) (rs: ireg) (imm: int64) (**r add immediate *) + | Pmake (rd: ireg) (imm: int) (**r load immediate *) + | Pmakel (rd: ireg) (imm: int64) (**r load immediate long *) + (** 64-bit integer register-register instructions *) - | Paddl (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) (* - | Psubl (rd: ireg) (rs1 rs2: ireg) (**r integer subtraction *) - - | Pmull (rd: ireg) (rs1 rs2: ireg) (**r integer multiply low *) - | Pmulhl (rd: ireg) (rs1 rs2: ireg) (**r integer multiply high signed *) - | Pmulhul (rd: ireg) (rs1 rs2: ireg) (**r integer multiply high unsigned *) - | Pdivl (rd: ireg) (rs1 rs2: ireg) (**r integer division *) - | Pdivul (rd: ireg) (rs1 rs2: ireg) (**r unsigned integer division *) - | Preml (rd: ireg) (rs1 rs2: ireg) (**r integer remainder *) - | Premul (rd: ireg) (rs1 rs2: ireg) (**r unsigned integer remainder *) - | Psltl (rd: ireg) (rs1 rs2: ireg) (**r set-less-than *) - | Psltul (rd: ireg) (rs1 rs2: ireg) (**r set-less-than unsigned *) - | Pseql (rd: ireg) (rs1 rs2: ireg) (**r [rd <- rs1 == rs2] (pseudo) *) - | Psnel (rd: ireg) (rs1 rs2: ireg) (**r [rd <- rs1 != rs2] (pseudo) *) - | Pandl (rd: ireg) (rs1 rs2: ireg) (**r bitwise and *) - | Porl (rd: ireg) (rs1 rs2: ireg) (**r bitwise or *) - | Pxorl (rd: ireg) (rs1 rs2: ireg) (**r bitwise xor *) - | Pslll (rd: ireg) (rs1 rs2: ireg) (**r shift-left-logical *) - | Psrll (rd: ireg) (rs1 rs2: ireg) (**r shift-right-logical *) - | Psral (rd: ireg) (rs1 rs2: ireg) (**r shift-right-arith *) - - | Pcvtl2w (rd: ireg) (rs: ireg) (**r int64->int32 (pseudo) *) - | Pcvtw2l (r: ireg) (**r int32 signed -> int64 (pseudo) *) + | Paddl (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) (* Unconditional jumps. Links are always to X1/RA. *) -*)| Pj_l (l: label) (**r jump to label *) -(*| Pj_s (symb: ident) (sg: signature) (**r jump to symbol *) - | Pj_r (r: ireg) (sg: signature) (**r jump register *) - | Pjal_s (symb: ident) (sg: signature) (**r jump-and-link symbol *) - | Pjal_r (r: ireg) (sg: signature) (**r jump-and-link register *) - - (* Conditional branches, 32-bit comparisons *) - | Pbeqw (rs1 rs2: ireg) (l: label) (**r branch-if-equal *) - | Pbnew (rs1 rs2: ireg) (l: label) (**r branch-if-not-equal signed *) - | Pbltw (rs1 rs2: ireg) (l: label) (**r branch-if-less signed *) - | Pbltuw (rs1 rs2: ireg) (l: label) (**r branch-if-less unsigned *) - | Pbgew (rs1 rs2: ireg) (l: label) (**r branch-if-greater-or-equal signed *) - | Pbgeuw (rs1 rs2: ireg) (l: label) (**r branch-if-greater-or-equal unsigned *) - - (* Conditional branches, 64-bit comparisons *) - | Pbeql (rs1 rs2: ireg) (l: label) (**r branch-if-equal *) - | Pbnel (rs1 rs2: ireg) (l: label) (**r branch-if-not-equal signed *) - | Pbltl (rs1 rs2: ireg) (l: label) (**r branch-if-less signed *) - | Pbltul (rs1 rs2: ireg) (l: label) (**r branch-if-less unsigned *) - | Pbgel (rs1 rs2: ireg) (l: label) (**r branch-if-greater-or-equal signed *) - | Pbgeul (rs1 rs2: ireg) (l: label) (**r branch-if-greater-or-equal unsigned *) - - (* Loads and stores *) - | Plb (rd: ireg) (ra: ireg) (ofs: offset) (**r load signed int8 *) - | Plbu (rd: ireg) (ra: ireg) (ofs: offset) (**r load unsigned int8 *) - | Plh (rd: ireg) (ra: ireg) (ofs: offset) (**r load signed int16 *) - | Plhu (rd: ireg) (ra: ireg) (ofs: offset) (**r load unsigned int16 *) -*)| Plw (rd: ireg) (ra: ireg) (ofs: offset) (**r load int32 *) + | Pj_l (l: label) (**r jump to label *) + + (* Conditional branches *) + | Pcb (bt: btest) (r: ireg) (l: label) (**r branch based on btest *) + + | Plw (rd: ireg) (ra: ireg) (ofs: offset) (**r load int32 *) | Plw_a (rd: ireg) (ra: ireg) (ofs: offset) (**r load any32 *) | Pld (rd: ireg) (ra: ireg) (ofs: offset) (**r load int64 *) | Pld_a (rd: ireg) (ra: ireg) (ofs: offset) (**r load any64 *) -(*| Psb (rs: ireg) (ra: ireg) (ofs: offset) (**r store int8 *) - | Psh (rs: ireg) (ra: ireg) (ofs: offset) (**r store int16 *) -*)| Psw (rs: ireg) (ra: ireg) (ofs: offset) (**r store int32 *) + | Psw (rs: ireg) (ra: ireg) (ofs: offset) (**r store int32 *) | Psw_a (rs: ireg) (ra: ireg) (ofs: offset) (**r store any32 *) | Psd (rs: ireg) (ra: ireg) (ofs: offset) (**r store int64 *) | Psd_a (rs: ireg) (ra: ireg) (ofs: offset) (**r store any64 *) @@ -600,6 +563,45 @@ Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: opti | None => Stuck end. +Inductive signedness: Type := Signed | Unsigned. + +Definition itest_for_cmp (c: comparison) (s: signedness) := + match c, s with + | Cne, Signed => ITne + | Ceq, Signed => ITeq + | Clt, Signed => ITlt + | Cge, Signed => ITge + | Cle, Signed => ITle + | Cgt, Signed => ITgt + | Cne, Unsigned => ITneu + | Ceq, Unsigned => ITequ + | Clt, Unsigned => ITltu + | Cge, Unsigned => ITgeu + | Cle, Unsigned => ITleu + | Cgt, Unsigned => ITgtu + end. + +(** Comparing integers *) +Definition compare_int (t: itest) (v1 v2: val) (m: mem): val := + match t with + | ITne => Val.cmp Cne v1 v2 + | ITeq => Val.cmp Ceq v1 v2 + | ITlt => Val.cmp Clt v1 v2 + | ITge => Val.cmp Cge v1 v2 + | ITle => Val.cmp Cle v1 v2 + | ITgt => Val.cmp Cgt v1 v2 + | ITneu => Val.cmpu (Mem.valid_pointer m) Cne v1 v2 + | ITequ => Val.cmpu (Mem.valid_pointer m) Ceq v1 v2 + | ITltu => Val.cmpu (Mem.valid_pointer m) Clt v1 v2 + | ITgeu => Val.cmpu (Mem.valid_pointer m) Cge v1 v2 + | ITleu => Val.cmpu (Mem.valid_pointer m) Cle v1 v2 + | ITgtu => Val.cmpu (Mem.valid_pointer m) Cgt v1 v2 + | ITall + | ITnall + | ITany + | ITnone => 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 @@ -633,90 +635,23 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmv d s => Next (nextinstr (rs#d <- (rs#s))) m +(** 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 + (** 32-bit integer register-immediate instructions *) | Paddiw d s i => Next (nextinstr (rs#d <- (Val.add rs##s (Vint i)))) m -(*| Psltiw d s i => - Next (nextinstr (rs#d <- (Val.cmp Clt rs##s (Vint i)))) m - | Psltiuw d s i => - Next (nextinstr (rs#d <- (Val.cmpu (Mem.valid_pointer m) Clt rs##s (Vint i)))) m - | Pandiw d s i => - Next (nextinstr (rs#d <- (Val.and rs##s (Vint i)))) m - | Poriw d s i => - Next (nextinstr (rs#d <- (Val.or rs##s (Vint i)))) m - | Pxoriw d s i => - Next (nextinstr (rs#d <- (Val.xor rs##s (Vint i)))) m - | Pslliw d s i => - Next (nextinstr (rs#d <- (Val.shl rs##s (Vint i)))) m - | Psrliw d s i => - Next (nextinstr (rs#d <- (Val.shru rs##s (Vint i)))) m - | Psraiw d s i => - Next (nextinstr (rs#d <- (Val.shr rs##s (Vint i)))) m - | Pluiw d i => - Next (nextinstr (rs#d <- (Vint (Int.shl i (Int.repr 12))))) m (** 32-bit integer register-register instructions *) -*)| Paddw d s1 s2 => + | Paddw d s1 s2 => Next (nextinstr (rs#d <- (Val.add rs##s1 rs##s2))) m -(*| Psubw d s1 s2 => - Next (nextinstr (rs#d <- (Val.sub rs##s1 rs##s2))) m - | Pmulw d s1 s2 => - Next (nextinstr (rs#d <- (Val.mul rs##s1 rs##s2))) m - | Pmulhw d s1 s2 => - Next (nextinstr (rs#d <- (Val.mulhs rs##s1 rs##s2))) m - | Pmulhuw d s1 s2 => - Next (nextinstr (rs#d <- (Val.mulhu rs##s1 rs##s2))) m - | Pdivw d s1 s2 => - Next (nextinstr (rs#d <- (Val.maketotal (Val.divs rs##s1 rs##s2)))) m - | Pdivuw d s1 s2 => - Next (nextinstr (rs#d <- (Val.maketotal (Val.divu rs##s1 rs##s2)))) m - | Premw d s1 s2 => - Next (nextinstr (rs#d <- (Val.maketotal (Val.mods rs##s1 rs##s2)))) m - | Premuw d s1 s2 => - Next (nextinstr (rs#d <- (Val.maketotal (Val.modu rs##s1 rs##s2)))) m - | Psltw d s1 s2 => - Next (nextinstr (rs#d <- (Val.cmp Clt rs##s1 rs##s2))) m - | Psltuw d s1 s2 => - Next (nextinstr (rs#d <- (Val.cmpu (Mem.valid_pointer m) Clt rs##s1 rs##s2))) m - | Pseqw d s1 s2 => - Next (nextinstr (rs#d <- (Val.cmpu (Mem.valid_pointer m) Ceq rs##s1 rs##s2))) m - | Psnew d s1 s2 => - Next (nextinstr (rs#d <- (Val.cmpu (Mem.valid_pointer m) Cne rs##s1 rs##s2))) m - | Pandw d s1 s2 => - Next (nextinstr (rs#d <- (Val.and rs##s1 rs##s2))) m - | Porw d s1 s2 => - Next (nextinstr (rs#d <- (Val.or rs##s1 rs##s2))) m - | Pxorw d s1 s2 => - Next (nextinstr (rs#d <- (Val.xor rs##s1 rs##s2))) m - | Psllw d s1 s2 => - Next (nextinstr (rs#d <- (Val.shl rs##s1 rs##s2))) m - | Psrlw d s1 s2 => - Next (nextinstr (rs#d <- (Val.shru rs##s1 rs##s2))) m - | Psraw d s1 s2 => - Next (nextinstr (rs#d <- (Val.shr rs##s1 rs##s2))) m (** 64-bit integer register-immediate instructions *) -*)| Paddil d s i => + | Paddil d s i => Next (nextinstr (rs#d <- (Val.addl rs###s (Vlong i)))) m -(*| Psltil d s i => - Next (nextinstr (rs#d <- (Val.maketotal (Val.cmpl Clt rs###s (Vlong i))))) m - | Psltiul d s i => - Next (nextinstr (rs#d <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt rs###s (Vlong i))))) m - | Pandil d s i => - Next (nextinstr (rs#d <- (Val.andl rs###s (Vlong i)))) m - | Poril d s i => - Next (nextinstr (rs#d <- (Val.orl rs###s (Vlong i)))) m - | Pxoril d s i => - Next (nextinstr (rs#d <- (Val.xorl rs###s (Vlong i)))) m - | Psllil d s i => - Next (nextinstr (rs#d <- (Val.shll rs###s (Vint i)))) m - | Psrlil d s i => - Next (nextinstr (rs#d <- (Val.shrlu rs###s (Vint i)))) m - | Psrail d s i => - Next (nextinstr (rs#d <- (Val.shrl rs###s (Vint i)))) m - | Pluil d i => - Next (nextinstr (rs#d <- (Vlong (Int64.sign_ext 32 (Int64.shl i (Int64.repr 12)))))) m -*)| Pmakel d i => + | Pmakel d i => Next (nextinstr (rs#d <- (Vlong i))) m | Pmake d i => Next (nextinstr (rs#d <- (Vint i))) m @@ -724,63 +659,18 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** 64-bit integer register-register instructions *) | Paddl d s1 s2 => Next (nextinstr (rs#d <- (Val.addl rs###s1 rs###s2))) m -(*| Psubl d s1 s2 => - Next (nextinstr (rs#d <- (Val.subl rs###s1 rs###s2))) m - | Pmull d s1 s2 => - Next (nextinstr (rs#d <- (Val.mull rs###s1 rs###s2))) m - | Pmulhl d s1 s2 => - Next (nextinstr (rs#d <- (Val.mullhs rs###s1 rs###s2))) m - | Pmulhul d s1 s2 => - Next (nextinstr (rs#d <- (Val.mullhu rs###s1 rs###s2))) m - | Pdivl d s1 s2 => - Next (nextinstr (rs#d <- (Val.maketotal (Val.divls rs###s1 rs###s2)))) m - | Pdivul d s1 s2 => - Next (nextinstr (rs#d <- (Val.maketotal (Val.divlu rs###s1 rs###s2)))) m - | Preml d s1 s2 => - Next (nextinstr (rs#d <- (Val.maketotal (Val.modls rs###s1 rs###s2)))) m - | Premul d s1 s2 => - Next (nextinstr (rs#d <- (Val.maketotal (Val.modlu rs###s1 rs###s2)))) m - | Psltl d s1 s2 => - Next (nextinstr (rs#d <- (Val.maketotal (Val.cmpl Clt rs###s1 rs###s2)))) m - | Psltul d s1 s2 => - Next (nextinstr (rs#d <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt rs###s1 rs###s2)))) m - | Pseql d s1 s2 => - Next (nextinstr (rs#d <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Ceq rs###s1 rs###s2)))) m - | Psnel d s1 s2 => - Next (nextinstr (rs#d <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Cne rs###s1 rs###s2)))) m - | Pandl d s1 s2 => - Next (nextinstr (rs#d <- (Val.andl rs###s1 rs###s2))) m - | Porl d s1 s2 => - Next (nextinstr (rs#d <- (Val.orl rs###s1 rs###s2))) m - | Pxorl d s1 s2 => - Next (nextinstr (rs#d <- (Val.xorl rs###s1 rs###s2))) m - | Pslll d s1 s2 => - Next (nextinstr (rs#d <- (Val.shll rs###s1 rs###s2))) m - | Psrll d s1 s2 => - Next (nextinstr (rs#d <- (Val.shrlu rs###s1 rs###s2))) m - | Psral d s1 s2 => - Next (nextinstr (rs#d <- (Val.shrl rs###s1 rs###s2))) m - - | Pcvtl2w d s => - Next (nextinstr (rs#d <- (Val.loword rs##s))) m - | Pcvtw2l r => - Next (nextinstr (rs#r <- (Val.longofint rs#r))) m - -(** Unconditional jumps. Links are always to X1/RA. *) -*)| Pj_l l => + +(** Unconditional jumps. *) + | Pj_l l => goto_label f l rs m -(*| Pj_s s sg => - Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m - | Pj_r r sg => - Next (rs#PC <- (rs#r)) m - | Pjal_s s sg => - Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero) - #RA <- (Val.offset_ptr rs#PC Ptrofs.one) - ) m - | Pjal_r r sg => - Next (rs#PC <- (rs#r) - #RA <- (Val.offset_ptr rs#PC Ptrofs.one) - ) m + +(** Conditional branches *) + | Pcb bt r l => + match bt with + | BTwnez => eval_branch f l rs m (Val.cmp_bool Cne rs##r (Vint (Int.repr 0))) + | _ => Stuck + end +(* (** Conditional branches, 32-bit comparisons *) | Pbeqw s1 s2 l => eval_branch f l rs m (Val.cmpu_bool (Mem.valid_pointer m) Ceq rs##s1 rs##s2) diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 69faf1f9..4b249f91 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -122,212 +122,18 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) := else addimm64 rd rs (Ptrofs.to_int64 n) k. -(* (** Translation of conditional branches. *) -Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg) (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: ireg) (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: ireg) (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: ireg) (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_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_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 transl_cbranch - (cond: condition) (args: list mreg) (lbl: label) (k: code) := + (cond: condition) (args: list mreg) (lbl: label) (k: code) : res (list instruction ) := 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 GPR0 lbl :: k - else - loadimm32 GPR31 n (transl_cbranch_int32s c r1 GPR31 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 GPR0 lbl :: k - else - loadimm32 GPR31 n (transl_cbranch_int32u c r1 GPR31 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 GPR0 lbl :: k - else - loadimm64 GPR31 n (transl_cbranch_int64s c r1 GPR31 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 GPR0 lbl :: k - else - loadimm64 GPR31 n (transl_cbranch_int64u c r1 GPR31 lbl :: k)) - | Ccompf c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c GPR31 r1 r2 in - OK (insn :: (if normal then Pbnew GPR31 GPR0 lbl else Pbeqw GPR31 GPR0 lbl) :: k) - | Cnotcompf c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c GPR31 r1 r2 in - OK (insn :: (if normal then Pbeqw GPR31 GPR0 lbl else Pbnew GPR31 GPR0 lbl) :: k) - | Ccompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c GPR31 r1 r2 in - OK (insn :: (if normal then Pbnew GPR31 GPR0 lbl else Pbeqw GPR31 GPR0 lbl) :: k) - | Cnotcompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c GPR31 r1 r2 in - OK (insn :: (if normal then Pbeqw GPR31 GPR0 lbl else Pbnew GPR31 GPR0 lbl) :: k) - | _, _ => - 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: ireg) (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: ireg) (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: ireg) (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: ireg) (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 GPR0 k else - match cmp with - | Ceq | Cne => xorimm32 rd r1 n (transl_cond_int32s cmp rd rd GPR0 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 GPR31 n (transl_cond_int32s cmp rd r1 GPR31 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 GPR0 k else - match cmp with - | Clt => sltuimm32 rd r1 n k - | _ => loadimm32 GPR31 n (transl_cond_int32u cmp rd r1 GPR31 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 GPR0 k else - match cmp with - | Ceq | Cne => xorimm64 rd r1 n (transl_cond_int64s cmp rd rd GPR0 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 GPR31 n (transl_cond_int64s cmp rd r1 GPR31 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 GPR0 k else - match cmp with - | Clt => sltuimm64 rd r1 n k - | _ => loadimm64 GPR31 n (transl_cond_int64u cmp rd r1 GPR31 k) - end. -*) - -Definition transl_cond_op - (cond: condition) (rd: ireg) (args: list mreg) (k: code) : res (list instruction) := - match cond, args with + OK (loadimm32 RTMP n (transl_comp c Unsigned r1 RTMP lbl k)) (*| Ccomp c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (transl_cond_int32s c rd r1 r2 k) @@ -337,9 +143,6 @@ Definition transl_cond_op | 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) @@ -369,7 +172,7 @@ Definition transl_cond_op 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") + Error(msg "Asmgen.transl_cbranch") end. (** Translation of the arithmetic operation [r <- op(args)]. @@ -839,9 +642,9 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) OK (Plabel lbl :: k) | Mgoto lbl => OK (Pj_l lbl :: k) -(*| Mcond cond args lbl => + | Mcond cond args lbl => transl_cbranch cond args lbl k - | Mjumptable arg tbl => do r <- ireg_of arg; OK (Pbtbl r tbl :: k) +(*| Mjumptable arg tbl => do r <- ireg_of arg; OK (Pbtbl r tbl :: k) *)| Mreturn => OK (make_epilogue f (Pret :: k)) (*OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: k))*) diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 068a2731..dd495cd4 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -174,12 +174,16 @@ Remark transl_cond_single_nolabel: Proof. unfold transl_cond_single; intros. destruct c; inv H; exact I. Qed. - +*) Remark transl_cbranch_label: forall cond args lbl k c, transl_cbranch cond args lbl k = OK c -> tail_nolabel k c. Proof. - intros. unfold transl_cbranch in H; destruct cond; TailNoLabel. + intros. unfold transl_cbranch in H. (* unfold transl_cond_op in H. *) destruct cond; TailNoLabel. + - unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel. +Qed. + +(* - destruct c0; simpl; TailNoLabel. - destruct c0; simpl; TailNoLabel. - destruct (Int.eq n Int.zero). @@ -212,8 +216,8 @@ Proof. - destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2. apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. destruct normal; TailNoLabel. -Qed. *) +(* Remark transl_cond_op_label: forall cond args r k c, transl_cond_op cond r args k = OK c -> tail_nolabel k c. @@ -270,7 +274,7 @@ Proof. destruct normal; TailNoLabel. *) Qed. - +*) Remark transl_op_label: forall op args r k c, transl_op op args r k = OK c -> tail_nolabel k c. @@ -373,6 +377,7 @@ Proof. - destruct s0; monadInv H; TailNoLabel. - destruct s0; monadInv H; eapply tail_nolabel_trans ; [eapply make_epilogue_label|TailNoLabel]. +- eapply transl_cbranch_label; eauto. - eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]. Qed. (* @@ -383,7 +388,6 @@ Qed. - destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I. - destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I. - destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]). -- eapply transl_cbranch_label; eauto. - eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]. *) @@ -899,24 +903,20 @@ Local Transparent destroyed_by_op. left; eapply exec_straight_opt_steps_goto; eauto. intros. simpl in TR. inversion TR. -(* exploit transl_cbranch_correct_true; eauto. intros (rs' & jmp & A & B & C). exists jmp; exists k; exists rs'. split. eexact A. split. apply agree_exten with rs0; auto with asmgen. exact B. -*) - (* Mcond false *) exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. left; eapply exec_straight_steps; eauto. intros. simpl in TR. inversion TR. -(* exploit transl_cbranch_correct_false; eauto. intros (rs' & A & B). exists rs'. split. eexact A. split. apply agree_exten with rs0; auto with asmgen. simpl. congruence. -*) - (* Mjumptable *) assert (f0 = f) by congruence. subst f0. inv AT. monadInv H6. diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v index b3965bb9..e16dbbaf 100644 --- a/mppa_k1c/Asmgenproof1.v +++ b/mppa_k1c/Asmgenproof1.v @@ -21,16 +21,16 @@ Require Import Op Locations Mach Conventions. Require Import Asm Asmgen Asmgenproof0. (** Decomposition of integer constants. *) -(* + Lemma make_immed32_sound: forall n, match make_immed32 n with | Imm32_single imm => n = imm - | Imm32_pair hi lo => n = Int.add (Int.shl hi (Int.repr 12)) lo end. Proof. intros; unfold make_immed32. set (lo := Int.sign_ext 12 n). - predSpec Int.eq Int.eq_spec n lo. + predSpec Int.eq Int.eq_spec n lo; auto. +(* - auto. - set (m := Int.sub n lo). assert (A: Int.eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto). @@ -54,8 +54,9 @@ Proof. rewrite Int.add_neg_zero. rewrite Int.add_zero. auto. rewrite (Int.modu_divu_Euclid m (Int.repr 4096)) at 1 by (vm_compute; congruence). rewrite D. apply Int.add_zero. -Qed. *) +Qed. + Lemma make_immed64_sound: forall n, match make_immed64 n with @@ -128,7 +129,7 @@ Proof. split. Simpl. intros; Simpl. Qed. - +*) Lemma loadimm32_correct: forall rd n k rs m, exists rs', @@ -140,11 +141,10 @@ Proof. destruct (make_immed32 n). - subst imm. econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split. rewrite Int.add_zero_l; Simpl. + split. Simpl. intros; Simpl. -- rewrite E. apply load_hilo32_correct. Qed. - +(* Lemma opimm32_correct: forall (op: ireg -> ireg0 -> ireg0 -> instruction) (opi: ireg -> ireg0 -> int -> instruction) @@ -281,7 +281,8 @@ Qed. Lemma addptrofs_correct_2: forall rd r1 n k (rs: regset) m b ofs, - r1 <> GPR31 -> rs#r1 = Vptr b ofs -> + r1 <> GPR31 -> rs#r1 = Vptr b of +s -> exists rs', exec_straight ge fn (addptrofs rd r1 n k) rs m k rs' m /\ rs'#rd = Vptr b (Ptrofs.add ofs n) @@ -294,91 +295,6 @@ Qed. (** Translation of conditional branches *) -Lemma transl_cbranch_int32s_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmp_bool cmp rs##r1 rs##r2 = Some b -> - exec_instr ge fn (transl_cbranch_int32s cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H. -- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H. - simpl; auto. -- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H. - simpl; auto. -- auto. -- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto. -- auto. -Qed. - -Lemma transl_cbranch_int32u_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 rs##r2 = Some b -> - exec_instr ge fn (transl_cbranch_int32u cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H; auto. -- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto. -Qed. - -Lemma transl_cbranch_int64s_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmpl_bool cmp rs###r1 rs###r2 = Some b -> - exec_instr ge fn (transl_cbranch_int64s cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H. -- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H. - simpl; auto. -- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H. - simpl; auto. -- auto. -- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto. -- auto. -Qed. - -Lemma transl_cbranch_int64u_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2 = Some b -> - exec_instr ge fn (transl_cbranch_int64u cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H; auto. -- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto. -Qed. - -Lemma transl_cond_float_correct: - forall (rs: regset) m cmp rd r1 r2 insn normal v, - transl_cond_float cmp rd r1 r2 = (insn, normal) -> - v = (if normal then Val.cmpf cmp rs#r1 rs#r2 else Val.notbool (Val.cmpf cmp rs#r1 rs#r2)) -> - exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m. -Proof. - intros. destruct cmp; simpl in H; inv H; auto. -- rewrite Val.negate_cmpf_eq. auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool. - rewrite <- Float.cmp_swap. auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool. - rewrite <- Float.cmp_swap. auto. -Qed. - -Lemma transl_cond_single_correct: - forall (rs: regset) m cmp rd r1 r2 insn normal v, - transl_cond_single cmp rd r1 r2 = (insn, normal) -> - v = (if normal then Val.cmpfs cmp rs#r1 rs#r2 else Val.notbool (Val.cmpfs cmp rs#r1 rs#r2)) -> - exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m. -Proof. - intros. destruct cmp; simpl in H; inv H; auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. - rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq f0 f); auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. - rewrite <- Float32.cmp_swap. auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. - rewrite <- Float32.cmp_swap. auto. -Qed. - Remark branch_on_GPR31: forall normal lbl (rs: regset) m b, rs#GPR31 = Val.of_bool (eqb normal b) -> @@ -388,6 +304,7 @@ Proof. intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. Qed. *) + Ltac ArgsInv := repeat (match goal with | [ H: Error _ = OK _ |- _ ] => discriminate @@ -417,7 +334,63 @@ Remark exec_straight_opt_right: Proof. destruct 1; intros. auto. eapply exec_straight_trans; eauto. Qed. -(* + +Lemma transl_comp_correct: + forall cmp r1 r2 lbl k rs m b, + exists rs', + exec_straight ge fn (transl_comp 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.cmp_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_comp. apply exec_straight_one; simpl; eauto. +- split. + + intros; Simpl. + + intros. + remember (nextinstr rs # GPR31 <- (compare_int (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_int (itest_for_cmp cmp Signed) rs ## r1 rs ## r2 m)). + { rewrite Heqrs'. auto. } + rewrite H0. rewrite <- H. + remember (Val.cmp_bool cmp rs##r1 rs##r2) as cmpbool. + destruct cmp; simpl; + unfold Val.cmp; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; + destruct b0; simpl; auto. + } + rewrite H0. simpl; auto. +Qed. + +Lemma transl_compu_correct: + forall cmp r1 r2 lbl k rs m b, + exists rs', + exec_straight ge fn (transl_comp 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.cmpu_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_comp. apply exec_straight_one; simpl; eauto. +- split. + + intros; Simpl. + + intros. + remember (nextinstr rs # GPR31 <- (compare_int (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_int (itest_for_cmp cmp Unsigned) rs ## r1 rs ## r2 m)). + { rewrite Heqrs'. auto. } + rewrite H0. rewrite <- H. + remember (Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 rs##r2) as cmpubool. + destruct cmp; simpl; unfold Val.cmpu; rewrite <- Heqcmpubool; destruct cmpubool; 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', transl_cbranch cond args lbl k = OK c -> @@ -427,7 +400,7 @@ Lemma transl_cbranch_correct_1: exists rs', exists insn, exec_straight_opt c rs m' (insn :: k) rs' m' /\ exec_instr ge fn insn rs' m' = eval_branch fn lbl rs' m' (Some b) - /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. Proof. intros until m'; intros TRANSL EVAL AG MEXT. set (vl' := map rs (map preg_of args)). @@ -435,84 +408,19 @@ Proof. { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. } clear EVAL MEXT AG. destruct cond; simpl in TRANSL; ArgsInv. -- exists rs, (transl_cbranch_int32s c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int32s_correct; auto. -- exists rs, (transl_cbranch_int32u c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int32u_correct; auto. -- predSpec Int.eq Int.eq_spec n Int.zero. -+ subst n. exists rs, (transl_cbranch_int32s c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int32s_correct; auto. -+ exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int32s c0 x GPR31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int32s_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- predSpec Int.eq Int.eq_spec n Int.zero. -+ subst n. exists rs, (transl_cbranch_int32u c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int32u_correct; auto. -+ exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int32u c0 x GPR31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int32u_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- exists rs, (transl_cbranch_int64s c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int64s_correct; auto. -- exists rs, (transl_cbranch_int64u c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int64u_correct; auto. -- predSpec Int64.eq Int64.eq_spec n Int64.zero. -+ subst n. exists rs, (transl_cbranch_int64s c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int64s_correct; auto. -+ exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int64s c0 x GPR31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int64s_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- predSpec Int64.eq Int64.eq_spec n Int64.zero. -+ subst n. exists rs, (transl_cbranch_int64u c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int64u_correct; auto. -+ exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int64u c0 x GPR31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int64u_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- destruct (transl_cond_float c0 GPR31 x x0) as [insn normal] eqn:TC; inv EQ2. - set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (eqb normal b)). - { unfold v, Val.cmpf. rewrite EVAL'. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. -- destruct (transl_cond_float c0 GPR31 x x0) as [insn normal] eqn:TC; inv EQ2. - assert (EVAL'': Val.cmpf_bool c0 (rs x) (rs x0) = Some (negb b)). - { destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. } - set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (xorb normal b)). - { unfold v, Val.cmpf. rewrite EVAL''. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. -- destruct (transl_cond_single c0 GPR31 x x0) as [insn normal] eqn:TC; inv EQ2. - set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (eqb normal b)). - { unfold v, Val.cmpfs. rewrite EVAL'. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. -- destruct (transl_cond_single c0 GPR31 x x0) as [insn normal] eqn:TC; inv EQ2. - assert (EVAL'': Val.cmpfs_bool c0 (rs x) (rs x0) = Some (negb b)). - { destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. } - set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (xorb normal b)). - { unfold v, Val.cmpfs. rewrite EVAL''. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. +- exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C). + exploit (transl_compu_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_comp c0 Unsigned x GPR31 lbl k)) (rs2 := rs') (m2 := m'). + eexact A. eexact A'. + + split; auto. + * apply C'; auto. unfold getw. rewrite B, C; eauto with asmgen. + * intros. rewrite B'; eauto with asmgen. Qed. + Lemma transl_cbranch_correct_true: forall cond args lbl k c m ms sp rs m', transl_cbranch cond args lbl k = OK c -> @@ -543,7 +451,7 @@ Proof. split. eapply exec_straight_opt_right; eauto. apply exec_straight_one; auto. intros; Simpl. Qed. - +(* (** Translation of condition operators *) Lemma transl_cond_int32s_correct: diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 280dd17b..2c7b8cc8 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -156,12 +156,36 @@ module Target : TARGET = | Ofsimm n -> ptrofs oc n | Ofslow(id, ofs) -> fprintf oc "%%lo(%a)" symbol_offset (id, ofs) + let icond_name = function + | ITne | ITneu -> "ne" + | ITeq | ITequ -> "eq" + | ITlt -> "lt" + | ITge -> "ge" + | ITle -> "le" + | ITgt -> "gt" + | ITltu -> "ltu" + | ITgeu -> "geu" + | ITleu -> "leu" + | ITgtu -> "gtu" + | ITall -> "all" + | ITnall -> "nall" + | ITany -> "any" + | ITnone -> "none" + + let icond oc c = fprintf oc "%s" (icond_name c) + + let bcond_name = function + | BTwnez -> "wnez" + | BTweqz -> "weqz" + + let bcond oc c = fprintf oc "%s" (bcond_name c) + (* Printing of instructions *) let print_instruction oc = function | Pcall(s) -> fprintf oc " call %a\n;;\n" symbol s | Pgoto(s) | Pj_l(s) -> - fprintf oc " goto %a\n;;\n" symbol s + fprintf oc " goto %a\n;;\n" print_label s | Pret -> fprintf oc " ret\n;;\n" | Pget (rd, rs) -> @@ -171,352 +195,41 @@ module Target : TARGET = | Pmv(rd, rs) -> fprintf oc " addd %a = %a, 0\n;;\n" ireg rd ireg rs - (* 32-bit integer register-immediate instructions *) | Paddiw (rd, rs, imm) -> fprintf oc " addd %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm - (*| Psltiw (rd, rs, imm) -> - fprintf oc " slti %a, %a, %a\n" ireg rd ireg rs coqint imm - | Psltiuw (rd, rs, imm) -> - fprintf oc " sltiu %a, %a, %a\n" ireg rd ireg rs coqint imm - | Pandiw (rd, rs, imm) -> - fprintf oc " andi %a, %a, %a\n" ireg rd ireg rs coqint imm - | Poriw (rd, rs, imm) -> - fprintf oc " ori %a, %a, %a\n" ireg rd ireg rs coqint imm - | Pxoriw (rd, rs, imm) -> - fprintf oc " xori %a, %a, %a\n" ireg rd ireg rs coqint imm - | Pslliw (rd, rs, imm) -> - fprintf oc " slli%t %a, %a, %a\n" w ireg rd ireg rs coqint imm - | Psrliw (rd, rs, imm) -> - fprintf oc " srli%t %a, %a, %a\n" w ireg rd ireg rs coqint imm - | Psraiw (rd, rs, imm) -> - fprintf oc " srai%t %a, %a, %a\n" w ireg rd ireg rs coqint imm - | Pluiw (rd, imm) -> - fprintf oc " lui %a, %a\n" ireg rd coqint imm - - (* 32-bit integer register-register instructions *) - *)| Paddw(rd, rs1, rs2) -> + | Paddw(rd, rs1, rs2) -> fprintf oc " addd %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 - (*| Psubw(rd, rs1, rs2) -> - fprintf oc " sub%t %a, %a, %a\n" w ireg rd ireg rs1 ireg rs2 - - | Pmulw(rd, rs1, rs2) -> - fprintf oc " mul%t %a, %a, %a\n" w ireg rd ireg rs1 ireg rs2 - | Pmulhw(rd, rs1, rs2) -> assert (not Archi.ptr64); - fprintf oc " mulh %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Pmulhuw(rd, rs1, rs2) -> assert (not Archi.ptr64); - fprintf oc " mulhu %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - - | Pdivw(rd, rs1, rs2) -> - fprintf oc " div%t %a, %a, %a\n" w ireg rd ireg rs1 ireg rs2 - | Pdivuw(rd, rs1, rs2) -> - fprintf oc " divu%t %a, %a, %a\n" w ireg rd ireg rs1 ireg rs2 - | Premw(rd, rs1, rs2) -> - fprintf oc " rem%t %a, %a, %a\n" w ireg rd ireg rs1 ireg rs2 - | Premuw(rd, rs1, rs2) -> - fprintf oc " remu%t %a, %a, %a\n" w ireg rd ireg rs1 ireg rs2 - - | Psltw(rd, rs1, rs2) -> - fprintf oc " slt %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Psltuw(rd, rs1, rs2) -> - fprintf oc " sltu %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - - | Pandw(rd, rs1, rs2) -> - fprintf oc " and %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Porw(rd, rs1, rs2) -> - fprintf oc " or %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Pxorw(rd, rs1, rs2) -> - fprintf oc " xor %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Psllw(rd, rs1, rs2) -> - fprintf oc " sll%t %a, %a, %a\n" w ireg rd ireg rs1 ireg rs2 - | Psrlw(rd, rs1, rs2) -> - fprintf oc " srl%t %a, %a, %a\n" w ireg rd ireg rs1 ireg rs2 - | Psraw(rd, rs1, rs2) -> - fprintf oc " sra%t %a, %a, %a\n" w ireg rd ireg rs1 ireg rs2 - - *)(* 64-bit integer register-immediate instructions *) | Paddil (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " addd %a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm - (*| Psltil (rd, rs, imm) -> assert Archi.ptr64; - fprintf oc " slti %a, %a, %a\n" ireg rd ireg rs coqint64 imm - | Psltiul (rd, rs, imm) -> assert Archi.ptr64; - fprintf oc " sltiu %a, %a, %a\n" ireg rd ireg rs coqint64 imm - | Pandil (rd, rs, imm) -> assert Archi.ptr64; - fprintf oc " andi %a, %a, %a\n" ireg rd ireg rs coqint64 imm - | Poril (rd, rs, imm) -> assert Archi.ptr64; - fprintf oc " ori %a, %a, %a\n" ireg rd ireg rs coqint64 imm - | Pxoril (rd, rs, imm) -> assert Archi.ptr64; - fprintf oc " xori %a, %a, %a\n" ireg rd ireg rs coqint64 imm - | Psllil (rd, rs, imm) -> assert Archi.ptr64; - fprintf oc " slli %a, %a, %a\n" ireg rd ireg rs coqint64 imm - | Psrlil (rd, rs, imm) -> assert Archi.ptr64; - fprintf oc " srli %a, %a, %a\n" ireg rd ireg rs coqint64 imm - | Psrail (rd, rs, imm) -> assert Archi.ptr64; - fprintf oc " srai %a, %a, %a\n" ireg rd ireg rs coqint64 imm - | Pluil (rd, imm) -> assert Archi.ptr64; - fprintf oc " lui %a, %a\n" ireg rd coqint64 imm - *) | Pmake (rd, imm) -> fprintf oc " make %a, %a\n;;\n" ireg rd coqint imm | Pmakel (rd, imm) -> fprintf oc " make %a, %a\n;;\n" ireg rd coqint64 imm - (* 64-bit integer register-register instructions *) | Paddl(rd, rs1, rs2) -> assert Archi.ptr64; fprintf oc " addd %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2 - (*| Psubl(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " sub %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - - | Pmull(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " mul %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Pmulhl(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " mulh %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Pmulhul(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " mulhu %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - - | Pdivl(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " div %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Pdivul(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " divu %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Preml(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " rem %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Premul(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " remu %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - - | Psltl(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " slt %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Psltul(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " sltu %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - - | Pandl(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " and %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Porl(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " or %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Pxorl(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " xor %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Pslll(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " sll %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Psrll(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " srl %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Psral(rd, rs1, rs2) -> assert Archi.ptr64; - fprintf oc " sra %a, %a, %a\n" ireg rd ireg rs1 ireg rs2 - - (* Unconditional jumps. Links are always to X1/RA. *) - (* TODO: fix up arguments for calls to variadics, to move *) - (* floating point arguments to integer registers. How? *) - | Pj_l(l) -> - fprintf oc " j %a\n" print_label l - | Pj_s(s, sg) -> - fprintf oc " j %a\n" symbol s - | Pj_r(r, sg) -> - fprintf oc " jr %a\n" ireg r - | Pjal_s(s, sg) -> - fprintf oc " call %a\n" symbol s - | Pjal_r(r, sg) -> - fprintf oc " jalr %a\n" ireg r - - (* Conditional branches, 32-bit comparisons *) - | Pbeqw(rs1, rs2, l) -> - fprintf oc " beq %a, %a, %a\n" ireg rs1 ireg rs2 print_label l - | Pbnew(rs1, rs2, l) -> - fprintf oc " bne %a, %a, %a\n" ireg rs1 ireg rs2 print_label l - | Pbltw(rs1, rs2, l) -> - fprintf oc " blt %a, %a, %a\n" ireg rs1 ireg rs2 print_label l - | Pbltuw(rs1, rs2, l) -> - fprintf oc " bltu %a, %a, %a\n" ireg rs1 ireg rs2 print_label l - | Pbgew(rs1, rs2, l) -> - fprintf oc " bge %a, %a, %a\n" ireg rs1 ireg rs2 print_label l - | Pbgeuw(rs1, rs2, l) -> - fprintf oc " bgeu %a, %a, %a\n" ireg rs1 ireg rs2 print_label l - - (* Conditional branches, 64-bit comparisons *) - | Pbeql(rs1, rs2, l) -> assert Archi.ptr64; - fprintf oc " beq %a, %a, %a\n" ireg rs1 ireg rs2 print_label l - | Pbnel(rs1, rs2, l) -> assert Archi.ptr64; - fprintf oc " bne %a, %a, %a\n" ireg rs1 ireg rs2 print_label l - | Pbltl(rs1, rs2, l) -> assert Archi.ptr64; - fprintf oc " blt %a, %a, %a\n" ireg rs1 ireg rs2 print_label l - | Pbltul(rs1, rs2, l) -> assert Archi.ptr64; - fprintf oc " bltu %a, %a, %a\n" ireg rs1 ireg rs2 print_label l - | Pbgel(rs1, rs2, l) -> assert Archi.ptr64; - fprintf oc " bge %a, %a, %a\n" ireg rs1 ireg rs2 print_label l - | Pbgeul(rs1, rs2, l) -> assert Archi.ptr64; - fprintf oc " bgeu %a, %a, %a\n" ireg rs1 ireg rs2 print_label l - - (* Loads and stores *) - | Plb(rd, ra, ofs) -> - fprintf oc " lb %a, %a(%a)\n" ireg rd offset ofs ireg ra - | Plbu(rd, ra, ofs) -> - fprintf oc " lbu %a, %a(%a)\n" ireg rd offset ofs ireg ra - | Plh(rd, ra, ofs) -> - fprintf oc " lh %a, %a(%a)\n" ireg rd offset ofs ireg ra - | Plhu(rd, ra, ofs) -> - fprintf oc " lhu %a, %a(%a)\n" ireg rd offset ofs ireg ra - *)| Plw(rd, ra, ofs) | Plw_a(rd, ra, ofs) | Pfls(rd, ra, ofs) -> - fprintf oc " lws %a = %a[%a]\n" ireg rd offset ofs ireg ra + + | Pcompw (it, rd, rs1, rs2) -> + fprintf oc " compw.%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 + + | Plw(rd, ra, ofs) | Plw_a(rd, ra, ofs) | Pfls(rd, ra, ofs) -> + fprintf oc " lws %a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra | Pld(rd, ra, ofs) | Pfld(rd, ra, ofs) | Pld_a(rd, ra, ofs) -> assert Archi.ptr64; fprintf oc " ld %a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra - - (*| Psb(rd, ra, ofs) -> - fprintf oc " sb %a, %a(%a)\n" ireg rd offset ofs ireg ra - | Psh(rd, ra, ofs) -> - fprintf oc " sh %a, %a(%a)\n" ireg rd offset ofs ireg ra - *)| Psw(rd, ra, ofs) | Psw_a(rd, ra, ofs) | Pfss(rd, ra, ofs) -> - fprintf oc " sw %a[%a] = %a\n" offset ofs ireg ra ireg rd + | Psw(rd, ra, ofs) | Psw_a(rd, ra, ofs) | Pfss(rd, ra, ofs) -> + fprintf oc " sw %a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd | Psd(rd, ra, ofs) | Psd_a(rd, ra, ofs) | Pfsd(rd, ra, ofs) -> assert Archi.ptr64; fprintf oc " sd %a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd - - (* Synchronization *) - (*| Pfence -> - fprintf oc " fence\n" - - (* floating point register move. - fmv.d preserves single-precision register contents, and hence - is applicable to both single- and double-precision moves. - *) - | Pfmv (fd,fs) -> - fprintf oc " fmv.d %a, %a\n" freg fd freg fs - | Pfmvxs (rd,fs) -> - fprintf oc " fmv.x.s %a, %a\n" ireg rd freg fs - | Pfmvxd (rd,fs) -> - fprintf oc " fmv.x.d %a, %a\n" ireg rd freg fs - - (* 32-bit (single-precision) floating point *) - | Pfls (fd, ra, ofs) -> - fprintf oc " flw %a, %a(%a)\n" freg fd offset ofs ireg ra - | Pfss (fs, ra, ofs) -> - fprintf oc " fsw %a, %a(%a)\n" freg fs offset ofs ireg ra - - | Pfnegs (fd, fs) -> - fprintf oc " fneg.s %a, %a\n" freg fd freg fs - | Pfabss (fd, fs) -> - fprintf oc " fabs.s %a, %a\n" freg fd freg fs - - | Pfadds (fd, fs1, fs2) -> - fprintf oc " fadd.s %a, %a, %a\n" freg fd freg fs1 freg fs2 - | Pfsubs (fd, fs1, fs2) -> - fprintf oc " fsub.s %a, %a, %a\n" freg fd freg fs1 freg fs2 - | Pfmuls (fd, fs1, fs2) -> - fprintf oc " fmul.s %a, %a, %a\n" freg fd freg fs1 freg fs2 - | Pfdivs (fd, fs1, fs2) -> - fprintf oc " fdiv.s %a, %a, %a\n" freg fd freg fs1 freg fs2 - | Pfmins (fd, fs1, fs2) -> - fprintf oc " fmin.s %a, %a, %a\n" freg fd freg fs1 freg fs2 - | Pfmaxs (fd, fs1, fs2) -> - fprintf oc " fmax.s %a, %a, %a\n" freg fd freg fs1 freg fs2 - - | Pfeqs (rd, fs1, fs2) -> - fprintf oc " feq.s %a, %a, %a\n" ireg rd freg fs1 freg fs2 - | Pflts (rd, fs1, fs2) -> - fprintf oc " flt.s %a, %a, %a\n" ireg rd freg fs1 freg fs2 - | Pfles (rd, fs1, fs2) -> - fprintf oc " fle.s %a, %a, %a\n" ireg rd freg fs1 freg fs2 - - | Pfsqrts (fd, fs) -> - fprintf oc " fsqrt.s %a, %a\n" freg fd freg fs - - | Pfmadds (fd, fs1, fs2, fs3) -> - fprintf oc " fmadd.s %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 - | Pfmsubs (fd, fs1, fs2, fs3) -> - fprintf oc " fmsub.s %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 - | Pfnmadds (fd, fs1, fs2, fs3) -> - fprintf oc " fnmadd.s %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 - | Pfnmsubs (fd, fs1, fs2, fs3) -> - fprintf oc " fnmsub.s %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 - - | Pfcvtws (rd, fs) -> - fprintf oc " fcvt.w.s %a, %a, rtz\n" ireg rd freg fs - | Pfcvtwus (rd, fs) -> - fprintf oc " fcvt.wu.s %a, %a, rtz\n" ireg rd freg fs - | Pfcvtsw (fd, rs) -> - fprintf oc " fcvt.s.w %a, %a\n" freg fd ireg rs - | Pfcvtswu (fd, rs) -> - fprintf oc " fcvt.s.wu %a, %a\n" freg fd ireg rs - - | Pfcvtls (rd, fs) -> assert Archi.ptr64; - fprintf oc " fcvt.l.s %a, %a, rtz\n" ireg rd freg fs - | Pfcvtlus (rd, fs) -> assert Archi.ptr64; - fprintf oc " fcvt.lu.s %a, %a, rtz\n" ireg rd freg fs - | Pfcvtsl (fd, rs) -> assert Archi.ptr64; - fprintf oc " fcvt.s.l %a, %a\n" freg fd ireg rs - | Pfcvtslu (fd, rs) -> assert Archi.ptr64; - fprintf oc " fcvt.s.lu %a, %a\n" freg fd ireg rs - - (* 64-bit (double-precision) floating point *) - | Pfld (fd, ra, ofs) | Pfld_a (fd, ra, ofs) -> - fprintf oc " fld %a, %a(%a)\n" freg fd offset ofs ireg ra - | Pfsd (fs, ra, ofs) | Pfsd_a (fs, ra, ofs) -> - fprintf oc " fsd %a, %a(%a)\n" freg fs offset ofs ireg ra - - | Pfnegd (fd, fs) -> - fprintf oc " fneg.d %a, %a\n" freg fd freg fs - | Pfabsd (fd, fs) -> - fprintf oc " fabs.d %a, %a\n" freg fd freg fs - - | Pfaddd (fd, fs1, fs2) -> - fprintf oc " fadd.d %a, %a, %a\n" freg fd freg fs1 freg fs2 - | Pfsubd (fd, fs1, fs2) -> - fprintf oc " fsub.d %a, %a, %a\n" freg fd freg fs1 freg fs2 - | Pfmuld (fd, fs1, fs2) -> - fprintf oc " fmul.d %a, %a, %a\n" freg fd freg fs1 freg fs2 - | Pfdivd (fd, fs1, fs2) -> - fprintf oc " fdiv.d %a, %a, %a\n" freg fd freg fs1 freg fs2 - | Pfmind (fd, fs1, fs2) -> - fprintf oc " fmin.d %a, %a, %a\n" freg fd freg fs1 freg fs2 - | Pfmaxd (fd, fs1, fs2) -> - fprintf oc " fmax.d %a, %a, %a\n" freg fd freg fs1 freg fs2 - - | Pfeqd (rd, fs1, fs2) -> - fprintf oc " feq.d %a, %a, %a\n" ireg rd freg fs1 freg fs2 - | Pfltd (rd, fs1, fs2) -> - fprintf oc " flt.d %a, %a, %a\n" ireg rd freg fs1 freg fs2 - | Pfled (rd, fs1, fs2) -> - fprintf oc " fle.d %a, %a, %a\n" ireg rd freg fs1 freg fs2 - - | Pfsqrtd (fd, fs) -> - fprintf oc " fsqrt.d %a, %a\n" freg fd freg fs - - | Pfmaddd (fd, fs1, fs2, fs3) -> - fprintf oc " fmadd.d %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 - | Pfmsubd (fd, fs1, fs2, fs3) -> - fprintf oc " fmsub.d %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 - | Pfnmaddd (fd, fs1, fs2, fs3) -> - fprintf oc " fnmadd.d %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 - | Pfnmsubd (fd, fs1, fs2, fs3) -> - fprintf oc " fnmsub.d %a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3 - - | Pfcvtwd (rd, fs) -> - fprintf oc " fcvt.w.d %a, %a, rtz\n" ireg rd freg fs - | Pfcvtwud (rd, fs) -> - fprintf oc " fcvt.wu.d %a, %a, rtz\n" ireg rd freg fs - | Pfcvtdw (fd, rs) -> - fprintf oc " fcvt.d.w %a, %a\n" freg fd ireg rs - | Pfcvtdwu (fd, rs) -> - fprintf oc " fcvt.d.wu %a, %a\n" freg fd ireg rs - - | Pfcvtld (rd, fs) -> assert Archi.ptr64; - fprintf oc " fcvt.l.d %a, %a, rtz\n" ireg rd freg fs - | Pfcvtlud (rd, fs) -> assert Archi.ptr64; - fprintf oc " fcvt.lu.d %a, %a, rtz\n" ireg rd freg fs - | Pfcvtdl (fd, rs) -> assert Archi.ptr64; - fprintf oc " fcvt.d.l %a, %a\n" freg fd ireg rs - | Pfcvtdlu (fd, rs) -> assert Archi.ptr64; - fprintf oc " fcvt.d.lu %a, %a\n" freg fd ireg rs - - | Pfcvtds (fd, fs) -> - fprintf oc " fcvt.d.s %a, %a\n" freg fd freg fs - | Pfcvtsd (fd, fs) -> - fprintf oc " fcvt.s.d %a, %a\n" freg fd freg fs - (* Pseudo-instructions expanded in Asmexpand *) - *)| Pallocframe(sz, ofs) -> + | Pallocframe(sz, ofs) -> assert false | Pfreeframe(sz, ofs) -> assert false - (*| Pseqw _ | Psnew _ | Pseql _ | Psnel _ | Pcvtl2w _ | Pcvtw2l _ -> - assert false (* Pseudo-instructions that remain *) - *)| Plabel lbl -> + | Plabel lbl -> fprintf oc "%a:\n" print_label lbl (*| Ploadsymbol(rd, id, ofs) -> loadsymbol oc rd id ofs diff --git a/test/mppa/Makefile b/test/mppa/Makefile index 9078bdb9..e73dcb38 100644 --- a/test/mppa/Makefile +++ b/test/mppa/Makefile @@ -1,4 +1,4 @@ -ELF=simple.bin call.bin +ELF=simple.bin call.bin branch.bin DEBUG:=$(if $(DEBUG),"-dall",) all: $(ELF) @@ -8,7 +8,7 @@ all: $(ELF) .SECONDARY: %.s: %.c - ccomp $(DEBUG) -v -S $< -o $@ + ccomp $(DEBUG) -O0 -v -S $< -o $@ .PHONY: clean: diff --git a/test/mppa/branch.c b/test/mppa/branch.c new file mode 100644 index 00000000..dee15568 --- /dev/null +++ b/test/mppa/branch.c @@ -0,0 +1,12 @@ +int main(void){ + int a=1; + int b; + + if(a){ + b = a+4; + } else { + b = a+2; + } + + return b; +} |