From cfdf756faa342378b7befd78d8288213f76c86e1 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 14 Jul 2015 22:41:44 +0200 Subject: Updated the branch and implemented the suggested changes. --- arm/Asm.v | 48 +++++++++++++++++++++++++++---------------- arm/Asmexpand.ml | 57 +++++++++++++++++++++++++++------------------------- arm/TargetPrinter.ml | 17 ++++++++++++++++ 3 files changed, 78 insertions(+), 44 deletions(-) (limited to 'arm') diff --git a/arm/Asm.v b/arm/Asm.v index dd434c02..4e8a411a 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -1,3 +1,4 @@ + (* *********************************************************************) (* *) (* The Compcert verified compiler *) @@ -206,23 +207,30 @@ Inductive instruction : Type := | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) | Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function *) | Pannot: external_function -> list (annot_arg preg) -> instruction (**r annotation statement *) - | Padc: ireg -> ireg -> shift_op -> instruction (**r add with carry *) - | Pcfi_adjust: int -> instruction (**r .cfi_adjust debug directive *) - | Pclz: preg -> preg -> instruction (**r count leading zeros. *) - | Pfsqrt: freg -> freg -> instruction (**r floating-point square root. *) - | Prev: preg -> preg -> instruction (**r reverse bytes and reverse bits. *) - | Prev16: preg -> preg -> instruction (**r reverse bytes and reverse bits. *) - | Prsc: ireg -> ireg -> shift_op -> instruction (**r reverse subtract without carry. *) - | Psbc: ireg -> ireg -> shift_op -> instruction (**r add with carry *) + | Padc: ireg -> ireg -> shift_op -> instruction (**r add with carry *) + | Pcfi_adjust: int -> instruction (**r .cfi_adjust debug directive *) + | Pclz: preg -> preg -> instruction (**r count leading zeros. *) + | Pfsqrt: freg -> freg -> instruction (**r floating-point square root. *) + | Prev: preg -> preg -> instruction (**r reverse bytes and reverse bits. *) + | Prev16: preg -> preg -> instruction (**r reverse bytes and reverse bits. *) + | Prsc: ireg -> ireg -> shift_op -> instruction (**r reverse subtract without carry. *) + | Psbc: ireg -> ireg -> shift_op -> instruction (**r add with carry *) (* Add, sub, rsb versions with s suffix *) - | Padds: ireg -> ireg -> shift_op -> instruction (**r integer addition with update of condition flags *) - | Psubs: ireg -> ireg -> shift_op -> instruction (**r integer subtraction with update of condition flags *) - | Prsbs: ireg -> ireg -> shift_op -> instruction (**r integer reverse subtraction with update of condition flags *) - | Pdmb: instruction (**r data memory barrier *) - | Pdsb: instruction (**r data synchronization barrier *) - | Pisb: instruction (**r instruction synchronization barrier *) - | Pbne: label -> instruction. (**r branch if negative macro *) - + | Padds: ireg -> ireg -> shift_op -> instruction (**r integer addition with update of condition flags *) + | Psubs: ireg -> ireg -> shift_op -> instruction (**r integer subtraction with update of condition flags *) + | Prsbs: ireg -> ireg -> shift_op -> instruction (**r integer reverse subtraction with update of condition flags *) + | Pdmb: instruction (**r data memory barrier *) + | Pdsb: instruction (**r data synchronization barrier *) + | Pisb: instruction (**r instruction synchronization barrier *) + | Pbne: label -> instruction (**r branch if negative macro *) + | Pldr_p: ireg -> ireg -> shift_op -> instruction (**r int32 load with post increment *) + | Pldrb_p: ireg -> ireg -> shift_op -> instruction (**r unsigned int8 load with post increment *) + | Pldrh_p: ireg -> ireg -> shift_op -> instruction (**r unsigned int16 load with post increment *) + | Pstr_p: ireg -> ireg -> shift_op -> instruction (**r int32 store with post increment *) + | Pstrb_p: ireg -> ireg -> shift_op -> instruction (**r unsigned int8 store with post increment *) + | Pstrh_p: ireg -> ireg -> shift_op -> instruction. (**r unsigned int16 store with post increment *) + + (** The pseudo-instructions are the following: @@ -758,7 +766,13 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pdmb | Pdsb | Pisb - | Pbne _ => + | Pbne _ + | Pldr_p _ _ _ + | Pldrb_p _ _ _ + | Pldrh_p _ _ _ + | Pstr_p _ _ _ + | Pstrb_p _ _ _ + | Pstrh_p _ _ _ => Stuck end. diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 95f35f37..b4508ace 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -91,22 +91,22 @@ let expand_annot_val txt targ args res = let expand_builtin_memcpy_small sz al src dst = let rec copy ofs sz = if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin - emit (Pfldd (FR7,src,ofs)); - emit (Pfstd (FR7,dst,ofs)); - copy (Int.add ofs _8) (sz - 8) - end else if sz >= 4 && al >= 4 then begin - emit (Pldr (IR14,src,SOimm ofs)); - emit (Pstr (IR14,dst,SOimm ofs)); - copy (Int.add ofs _4) (sz - 4) - end else if sz >= 2 && al >= 2 then begin - emit (Pldrh (IR14,src,SOimm ofs)); - emit (Pstrh (IR14,dst,SOimm ofs)); - copy (Int.add ofs _2) (sz - 2) - end else if sz >= 1 then begin - emit (Pldrb (IR14,src,SOimm ofs)); - emit (Pstrb (IR14,dst,SOimm ofs)); - copy (Int.add ofs _1) (sz - 1) - end else + emit (Pfldd (FR7,src,ofs)); + emit (Pfstd (FR7,dst,ofs)); + copy (Int.add ofs _8) (sz - 8) + end else if sz >= 4 && al >= 4 then begin + emit (Pldr (IR14,src,SOimm ofs)); + emit (Pstr (IR14,dst,SOimm ofs)); + copy (Int.add ofs _4) (sz - 4) + end else if sz >= 2 && al >= 2 then begin + emit (Pldrh (IR14,src,SOimm ofs)); + emit (Pstrh (IR14,dst,SOimm ofs)); + copy (Int.add ofs _2) (sz - 2) + end else if sz >= 1 then begin + emit (Pldrb (IR14,src,SOimm ofs)); + emit (Pstrb (IR14,dst,SOimm ofs)); + copy (Int.add ofs _1) (sz - 1) + end else () in copy _0 sz @@ -116,9 +116,9 @@ let expand_builtin_memcpy_big sz al src dst = assert (src = IR2); assert (dst = IR3); let (load, store, chunksize) = - if al >= 4 then (Pldr (IR12,src,SOimm _4), Pstr (IR12,dst,SOimm _4) , 4) - else if al = 2 then (Pldrh (IR12,src,SOimm _2), Pstrh (IR12,dst,SOimm _2), 2) - else (Pldrb (IR12,src,SOimm _1), Pstrb (IR12,dst,SOimm _1), 1) in + if al >= 4 then (Pldr_p (IR12,src,SOimm _4), Pstr_p (IR12,dst,SOimm _4) , 4) + else if al = 2 then (Pldrh_p (IR12,src,SOimm _2), Pstrh_p (IR12,dst,SOimm _2), 2) + else (Pldrb_p (IR12,src,SOimm _1), Pstrb_p (IR12,dst,SOimm _1), 1) in expand_movimm IR14 (coqint_of_camlint (Int32.of_int (sz / chunksize))); let lbl = new_label () in emit (Plabel lbl); @@ -239,14 +239,17 @@ let expand_builtin_inline name args res = emit (Pfsqrt (res,a1)) (* 64-bit integer arithmetic *) | "__builtin_negl", [IR ah;IR al], [IR rh; IR rl] -> - emit (Prsbs (rl,al,SOimm _0)); - if !Clflags.option_mthumb then begin - emit (Pmvn (rh,SOreg ah)); - emit (Padc (rh,rh,SOimm _0)) - end else - begin - emit (Prsc (rh,ah,SOimm _0)) - end + expand_int64_arith (rl = ah ) rl (fun rl -> + emit (Prsbs (rl,al,SOimm _0)); + (* No "rsc" instruction in Thumb2. Emulate based on + rsc a, b, #0 == a <- AddWithCarry(~b, 0, carry) + == mvn a, b; adc a, a, #0 *) + if !Clflags.option_mthumb then begin + emit (Pmvn (rh,SOreg ah)); + emit (Padc (rh,rh,SOimm _0)) + end else begin + emit (Prsc (rh,ah,SOimm _0)) + end) | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> expand_int64_arith (rl = ah || rl = bh) rl (fun rl -> diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 88261940..f8d72836 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -539,6 +539,12 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " ldrb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 | Pldrh(r1, r2, sa) -> fprintf oc " ldrh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + | Pldr_p(r1, r2, sa) -> + fprintf oc " ldr %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + | Pldrb_p(r1, r2, sa) -> + fprintf oc " ldrb %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + | Pldrh_p(r1, r2, sa) -> + fprintf oc " ldrh %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 | Pldrsb(r1, r2, sa) -> fprintf oc " ldrsb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 | Pldrsh(r1, r2, sa) -> @@ -591,6 +597,17 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " strb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 | Pstrh(r1, r2, sa) -> fprintf oc " strh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + | Pstr_p(r1, r2, sa) -> + fprintf oc " str %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; + begin match r1, r2, sa with + | IR14, IR13, SOimm n -> cfi_rel_offset oc "lr" (camlint_of_coqint n) + | _ -> () + end; + 1 + | Pstrb_p(r1, r2, sa) -> + fprintf oc " strb %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + | Pstrh_p(r1, r2, sa) -> + fprintf oc " strh %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 | Psdiv -> if Opt.hardware_idiv then begin fprintf oc " sdiv r0, r0, r1\n"; 1 -- cgit