aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/Asm.v12
-rw-r--r--powerpc/AsmToJSON.ml9
-rw-r--r--powerpc/Asmexpand.ml6
-rw-r--r--powerpc/CBuiltins.ml9
-rw-r--r--powerpc/ConstpropOp.vp14
-rw-r--r--powerpc/ConstpropOpproof.v28
-rw-r--r--powerpc/TargetPrinter.ml6
-rw-r--r--powerpc/ValueAOp.v4
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
generated by cgit (git 2.34.1) at 2024-07-09 18:15:55 +0000