diff options
| -rw-r--r-- | powerpc/Asm.v | 2 | ||||
| -rw-r--r-- | powerpc/AsmToJSON.ml | 7 | ||||
| -rw-r--r-- | powerpc/Asmexpand.ml | 2 | ||||
| -rw-r--r-- | powerpc/CBuiltins.ml | 2 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 2 |
5 files changed, 12 insertions, 3 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index a1d8338a..cd4c8d00 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -270,6 +270,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 *) @@ -870,6 +871,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Plwarx _ _ _ | Plwbrx _ _ _ | Pisync + | Plwsync | Plhbrx _ _ _ | Plwzu _ _ _ | Pmfcr _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 520bc1ed..ea627b9b 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -211,12 +211,13 @@ let p_instruction oc ic = | 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 | 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 +350,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 fd252b98..487aaaae 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -416,6 +416,8 @@ let expand_builtin_inline name args res = emit (Psync) | "__builtin_isync", [], _ -> emit (Pisync) + | "__builtin_lwsync", [], _ -> + emit (Plwsync) | "__builtin_trap", [], _ -> emit (Ptrap) (* Vararg stuff *) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 222a4d94..f1f57644 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -83,6 +83,8 @@ let builtins = { (TVoid [], [], false); "__builtin_isync", (TVoid [], [], false); + "__builtin_lwsync", + (TVoid [], [], false); "__builtin_trap", (TVoid [], [], false) ] diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 1cd7fe37..cffb4496 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -537,6 +537,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 | 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) -> |