diff options
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/Asm.v | 12 | ||||
-rw-r--r-- | powerpc/AsmToJSON.ml | 9 | ||||
-rw-r--r-- | powerpc/Asmexpand.ml | 6 | ||||
-rw-r--r-- | powerpc/CBuiltins.ml | 9 | ||||
-rw-r--r-- | powerpc/ConstpropOp.vp | 14 | ||||
-rw-r--r-- | powerpc/ConstpropOpproof.v | 28 | ||||
-rw-r--r-- | powerpc/TargetPrinter.ml | 6 | ||||
-rw-r--r-- | powerpc/ValueAOp.v | 4 |
8 files changed, 57 insertions, 31 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index a1d8338a..f1e84146 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -161,10 +161,11 @@ Inductive instruction : Type := | Pcmplwi: ireg -> constant -> instruction (**r same, with immediate argument *) | Pcmpw: ireg -> ireg -> instruction (**r signed integer comparison *) | Pcmpwi: ireg -> constant -> instruction (**r same, with immediate argument *) - | Pcntlzw: ireg -> ireg -> instruction (**r count leading zeros *) + | Pcntlzw: ireg -> ireg -> instruction (**r count leading zeros *) | Pcreqv: crbit -> crbit -> crbit -> instruction (**r not-xor between condition bits *) | Pcror: crbit -> crbit -> crbit -> instruction (**r or between condition bits *) | Pcrxor: crbit -> crbit -> crbit -> instruction (**r xor between condition bits *) + | Pdcbi: ireg -> ireg -> instruction (**r data cache invalidate *) | Pdivw: ireg -> ireg -> ireg -> instruction (**r signed division *) | Pdivwu: ireg -> ireg -> ireg -> instruction (**r unsigned division *) | Peieio: instruction (**r EIEIO barrier *) @@ -201,6 +202,7 @@ Inductive instruction : Type := | Pfres: freg -> freg -> instruction (**r approximate inverse *) | Pfsel: freg -> freg -> freg -> freg -> instruction (**r FP conditional move *) | Pisync: instruction (**r ISYNC barrier *) + | Picbi: ireg -> ireg -> instruction (**r instruction cache invalidate *) | Plbz: ireg -> constant -> ireg -> instruction (**r load 8-bit unsigned int *) | Plbzx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Plfd: freg -> constant -> ireg -> instruction (**r load 64-bit float *) @@ -270,6 +272,7 @@ Inductive instruction : Type := | Psubfze: ireg -> ireg -> instruction (**r integer opposite with carry *) | Psubfic: ireg -> ireg -> constant -> instruction (**r integer subtraction from immediate *) | Psync: instruction (**r SYNC barrier *) + | Plwsync: instruction (**r LWSYNC barrier *) | Ptrap: instruction (**r unconditional trap *) | Pxor: ireg -> ireg -> ireg -> instruction (**r bitwise xor *) | Pxori: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate *) @@ -856,6 +859,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pcntlzw _ _ | Pcreqv _ _ _ | Pcrxor _ _ _ + | Pdcbi _ _ | Peieio | Pfctiw _ _ | Pfctiwz _ _ @@ -869,7 +873,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfsel _ _ _ _ | Plwarx _ _ _ | Plwbrx _ _ _ + | Picbi _ _ | Pisync + | Plwsync | Plhbrx _ _ _ | Plwzu _ _ _ | Pmfcr _ @@ -1060,6 +1066,4 @@ Definition data_preg (r: preg) : bool := | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false | CARRY => false | _ => true - end. - - + end.
\ No newline at end of file diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 520bc1ed..81ffd500 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -175,6 +175,7 @@ let p_instruction oc ic = | Pcreqv (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcreqv\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 | Pcror (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcror\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 | Pcrxor (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcrxor\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 + | Pdcbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pdivw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pdivwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Peieio -> fprintf oc "{\"Instruction Name\":\"Peieio,\"Args\":[]}" @@ -210,13 +211,15 @@ let p_instruction oc ic = | Pfrsqrte (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfsqrte\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfres (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfres\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfsel (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfsel\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 + | Picbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":[]}" + | Plwsync -> fprintf oc "{\"Instruction Name\":\"Plwsync\",\"Args\":[]}" | Plbz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Plbzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pblzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Plfd (fr,c,ir) | Plfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plfd\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir - | Plfdx (fr,ir1,ir2) - | Plfdx_a (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfdx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Plfdx (fr,ir1,ir2) + | Plfdx_a (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfdx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 | Plfs (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plfs\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir | Plfsx (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfsx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 | Plha (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plha\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 @@ -349,7 +352,7 @@ let p_vardef oc (name,v) = fprintf oc "{\"Var Name\":%a,\"Var Readonly\":%B,\"Var Volatile\":%B,\n\"Var Storage Class\":%a,\n\"Var Alignment\":%a,\n\"Var Section\":%a,\n\"Var Init\":%a}\n" p_atom name v.gvar_readonly v.gvar_volatile p_storage static p_int_opt alignment p_section section - (p_list p_init_data) v.gvar_init + (p_list p_init_data) v.gvar_init let p_program oc prog = let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) -> diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index b8d30ae3..976f4e77 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -386,12 +386,18 @@ let expand_builtin_inline name args res = emit (Psync) | "__builtin_isync", [], _ -> emit (Pisync) + | "__builtin_lwsync", [], _ -> + emit (Plwsync) | "__builtin_trap", [], _ -> emit (Ptrap) (* Vararg stuff *) | "__builtin_va_start", [IR a], _ -> expand_builtin_va_start a (* Catch-all *) + | "__builtin_dcbi", [IR a1],_ -> + emit (Pdcbi (GPR0,a1)) + | "__builtin_icbi", [IR a1],_ -> + emit (Picbi(GPR0,a1)) | _ -> invalid_arg ("unrecognized builtin " ^ name) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 222a4d94..e774614e 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -83,8 +83,15 @@ let builtins = { (TVoid [], [], false); "__builtin_isync", (TVoid [], [], false); + "__builtin_lwsync", + (TVoid [], [], false); "__builtin_trap", - (TVoid [], [], false) + (TVoid [], [], false); + (* Cache isntructions *) + "__builtin_dcbi", + (TVoid [],[TPtr(TVoid [], [])],false); + "__builtin_icbi", + (TVoid [],[TPtr(TVoid [], [])],false) ] } diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index bba0fad4..7265337d 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -52,12 +52,12 @@ Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) := Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) := match c, args, vl with | Ccompimm Ceq n, r1 :: nil, v1 :: nil => - if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil) + if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) else make_cmp_base c args vl | Ccompimm Cne n, r1 :: nil, v1 :: nil => - if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil) + if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) else make_cmp_base c args vl | _, _, _ => make_cmp_base c args vl @@ -120,7 +120,7 @@ Definition make_divuimm (n: int) (r1 r2: reg) := Definition make_andimm (n: int) (r: reg) (a: aval) := if Int.eq n Int.zero then (Ointconst Int.zero, nil) else if Int.eq n Int.mone then (Omove, r :: nil) - else if match a with Uns m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero + else if match a with Uns _ m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero | _ => false end then (Omove, r :: nil) else (Oandimm n, r :: nil). @@ -146,9 +146,9 @@ Definition make_mulfsimm (n: float32) (r r1 r2: reg) := else (Omulfs, r1 :: r2 :: nil). Definition make_cast8signed (r: reg) (a: aval) := - if vincl a (Sgn 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). + if vincl a (Sgn Ptop 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). Definition make_cast16signed (r: reg) (a: aval) := - if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). + if vincl a (Sgn Ptop 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 8498868a..aac37dc6 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -131,24 +131,24 @@ Lemma make_cmp_correct: /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v. Proof. intros c args vl. - assert (Y: forall r, vincl (AE.get r ae) (Uns 1) = true -> + assert (Y: forall r, vincl (AE.get r ae) (Uns Ptop 1) = true -> rs#r = Vundef \/ rs#r = Vint Int.zero \/ rs#r = Vint Int.one). - { intros. apply vmatch_Uns_1 with bc. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. } + { intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. } unfold make_cmp. case (make_cmp_match c args vl); intros. -- destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1. +- destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. simpl in H; inv H. InvBooleans. subst n. exists (rs#r1); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. - destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0. + destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. simpl in H; inv H. InvBooleans. subst n. exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. apply make_cmp_base_correct; auto. -- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0. +- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. simpl in H; inv H. InvBooleans. subst n. exists (rs#r1); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. - destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1. + destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. simpl in H; inv H. InvBooleans. subst n. exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. @@ -271,7 +271,7 @@ Proof. subst n. exists (Vint Int.zero); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone; intros. subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_mone; auto. - destruct (match x with Uns k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero + destruct (match x with Uns _ k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero | _ => false end) eqn:UNS. destruct x; try congruence. exists (rs#r); split; auto. @@ -282,7 +282,7 @@ Proof. rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. rewrite Int.bits_not by auto. apply negb_involutive. - rewrite H5 by auto. auto. + rewrite H6 by auto. auto. econstructor; split; eauto. auto. Qed. @@ -372,11 +372,11 @@ Lemma make_cast8signed_correct: let (op, args) := make_cast8signed r x in exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v. Proof. - intros; unfold make_cast8signed. destruct (vincl x (Sgn 8)) eqn:INCL. + intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL. exists rs#r; split; auto. - assert (V: vmatch bc rs#r (Sgn 8)). + assert (V: vmatch bc rs#r (Sgn Ptop 8)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto. + inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. econstructor; split; simpl; eauto. Qed. @@ -386,11 +386,11 @@ Lemma make_cast16signed_correct: let (op, args) := make_cast16signed r x in exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v. Proof. - intros; unfold make_cast16signed. destruct (vincl x (Sgn 16)) eqn:INCL. + intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL. exists rs#r; split; auto. - assert (V: vmatch bc rs#r (Sgn 16)). + assert (V: vmatch bc rs#r (Sgn Ptop 16)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto. + inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. econstructor; split; simpl; eauto. Qed. diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 1cd7fe37..cb3ce87a 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -469,6 +469,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " cror %a, %a, %a\n" crbit c1 crbit c2 crbit c3 | Pcrxor(c1, c2, c3) -> fprintf oc " crxor %a, %a, %a\n" crbit c1 crbit c2 crbit c3 + | Pdcbi (r1,r2) -> + fprintf oc " dcbi %a, %a\n" ireg r1 ireg r2 | Pdivw(r1, r2, r3) -> fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pdivwu(r1, r2, r3) -> @@ -535,8 +537,12 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fres %a, %a\n" freg r1 freg r2 | Pfsel(r1, r2, r3, r4) -> fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Picbi (r1,r2) -> + fprintf oc " icbi %a,%a\n" ireg r1 ireg r2 | Pisync -> fprintf oc " isync\n" + | Plwsync -> + fprintf oc " lwsync\n" | Plbz(r1, c, r2) -> fprintf oc " lbz %a, %a(%a)\n" ireg r1 constant c ireg r2 | Plbzx(r1, r2, r3) -> diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index a5a1db80..8cb29145 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -51,8 +51,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 | Ointconst n, nil => I n - | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop - | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop + | Ofloatconst n, nil => if propagate_float_constants tt then F n else ntop + | Osingleconst n, nil => if propagate_float_constants tt then FS n else ntop | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs) | Oaddrstack ofs, nil => Ptr (Stk ofs) | Ocast8signed, v1 :: nil => sign_ext 8 v1 |