From 4eb7fcaf6a5e366c71d95d2152dcc1f3982c404b Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Fri, 14 Aug 2015 15:12:40 +0200
Subject: Added builtin for the lwsync barrier.

---
 powerpc/Asm.v            | 2 ++
 powerpc/AsmToJSON.ml     | 7 ++++---
 powerpc/Asmexpand.ml     | 2 ++
 powerpc/CBuiltins.ml     | 2 ++
 powerpc/TargetPrinter.ml | 2 ++
 5 files changed, 12 insertions(+), 3 deletions(-)

(limited to 'powerpc')

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) ->
-- 
cgit