diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-11 12:05:31 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-11 12:05:31 +0200 |
| commit | 0de3d126e70dfedfd6f74710da31c4b9636f900a (patch) | |
| tree | 43b19f66ef97def541881bceebcbdac4cfca8fb2 /powerpc | |
| parent | 2809e264a4c146b31b5009fba08f74d12126a1b3 (diff) | |
| download | compcert-0de3d126e70dfedfd6f74710da31c4b9636f900a.tar.gz compcert-0de3d126e70dfedfd6f74710da31c4b9636f900a.zip | |
Use the gcc version of atomic load.
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Asm.v | 2 | ||||
| -rw-r--r-- | powerpc/AsmToJSON.ml | 3 | ||||
| -rw-r--r-- | powerpc/Asmexpand.ml | 4 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 5 |
4 files changed, 10 insertions, 4 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 66bb4607..5fd40a27 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -154,6 +154,7 @@ Inductive instruction : Type := | Pbf: crbit -> label -> instruction (**r branch if false *) | Pbl: ident -> signature -> instruction (**r branch and link *) | Pbne: label -> instruction (**r branch not equal *) + | Pbne_rel: int -> instruction (**r branch not equal with relative offset *) | Pbs: ident -> signature -> instruction (**r branch to symbol *) | Pblr: instruction (**r branch to contents of register LR *) | Pbt: crbit -> label -> instruction (**r branch if true *) @@ -875,6 +876,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out directly by [Asmgen], so we do not model them. *) | Pbdnz _ | Pbne _ + | Pbne_rel _ | Pcmpb _ _ _ | Pcntlzw _ _ | Pcreqv _ _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 7064ebdd..d23beaad 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -163,7 +163,8 @@ let p_instruction oc ic = | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l | Pbf (c,l) -> fprintf oc "{\"Instruction Name\":\"Pbf\",\"Args\":[%a,%a]}" p_crbit c p_label l | Pbl (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbl\",\"Args\":[%a]}" p_atom_constant i - | Pbne (lbl) -> fprintf oc "{\"Instruction Name\":\"Pbne\",\"Args\":[%a]}" p_label lbl + | Pbne lbl -> fprintf oc "{\"Instruction Name\":\"Pbne\",\"Args\":[%a]}" p_label lbl + | Pbne_rel ofs -> fprintf oc"{\"Instruction Name\":\"Pbne_rel\",\"Args\":[%a]}" p_int_constant ofs | Pbs (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbs\",\"Args\":[%a]}" p_atom_constant i | Pblr -> fprintf oc "{\"Instruction Name\":\"Pblr\",\"Args\":[]}" | Pbt (cr,l) -> fprintf oc "{\"Instruction Name\":\"Pbt\",\"Args\":[%a,%a]}" p_crbit cr p_label l diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 8cd123fe..5e26e8a6 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -499,12 +499,10 @@ let expand_builtin_inline name args res = emit (Pisync); emit (Pstw (GPR11,Cint _0,a3)) | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ -> - let lbl = new_label() in emit (Psync); - emit (Plabel lbl); emit (Plwz (a1,Cint _0,a1)); emit (Pcmpw (a1,a1)); - emit (Pbne lbl); + emit (Pbne_rel _4); emit (Pisync); emit (Pstw (a1,Cint _0, a2)); | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) -> diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index f5295777..1f1306c0 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -416,6 +416,11 @@ module Target (System : SYSTEM):TARGET = fprintf oc " bl %a\n" symbol s | Pbne lbl -> fprintf oc " bne- %a\n" label (transl_label lbl) + | Pbne_rel ofs -> + let ofs = camlint_of_coqint ofs in + let sign = if ofs >= 0l then "+" else "-" in + let ofs = Int32.abs ofs in + fprintf oc " bne- $%s%ld\n" sign ofs | Pbs(s, sg) -> fprintf oc " b %a\n" symbol s | Pblr -> |