Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-non-trapping-load

1 files changed, 19 insertions, 18 deletions

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 0ef0a21e..704b0aba 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -14,6 +14,7 @@
    of the PPC assembly code. *)
 
 open Camlcoq
+open! Integers
 open AST
 open Asm
 open Asmexpandaux
@@ -29,8 +30,8 @@ let eref =
 
 (* Useful constants and helper functions *)
 
-let _0 = Integers.Int.zero
-let _1 = Integers.Int.one
+let _0 = Int.zero
+let _1 = Int.one
 let _2 = coqint_of_camlint 2l
 let _4 = coqint_of_camlint 4l
 let _6 = coqint_of_camlint 6l
@@ -44,7 +45,7 @@ let _m4 = coqint_of_camlint (-4l)
 let _m8 = coqint_of_camlint (-8l)
 let _m16 = coqint_of_camlint (-16l)
 
-let _0L = Integers.Int64.zero
+let _0L = Int64.zero
 let _32L = coqint_of_camlint64 32L
 let _64L = coqint_of_camlint64 64L
 let _m1L = coqint_of_camlint64 (-1L)
@@ -88,7 +89,7 @@ let expand_annot_val kind txt targ args res =
    Note that lfd and stfd cannot trap on ill-formed floats. *)
 
 let offset_in_range ofs =
-  Integers.Int.eq (Asmgen.high_s ofs) _0
+  Int.eq (Asmgen.high_s ofs) _0
 
 let memcpy_small_arg sz arg tmp =
   match arg with
@@ -96,7 +97,7 @@ let memcpy_small_arg sz arg tmp =
       (r, _0)
   | BA_addrstack ofs ->
       if offset_in_range ofs
-      && offset_in_range (Integers.Int.add ofs (Integers.Int.repr (Z.of_uint sz)))
+      && offset_in_range (Int.add ofs (Int.repr (Z.of_uint sz)))
       then (GPR1, ofs)
       else begin emit_addimm tmp GPR1 ofs; (tmp, _0) end
   | _ ->
@@ -111,19 +112,19 @@ let expand_builtin_memcpy_small sz al src dst =
     if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin
       emit (Plfd(FPR13, Cint osrc, rsrc));
       emit (Pstfd(FPR13, Cint odst, rdst));
-      copy (Integers.Int.add osrc _8) (Integers.Int.add odst _8) (sz - 8)
+      copy (Int.add osrc _8) (Int.add odst _8) (sz - 8)
     end else if sz >= 4 then begin
       emit (Plwz(GPR0, Cint osrc, rsrc));
       emit (Pstw(GPR0, Cint odst, rdst));
-      copy (Integers.Int.add osrc _4) (Integers.Int.add odst _4) (sz - 4)
+      copy (Int.add osrc _4) (Int.add odst _4) (sz - 4)
     end else if sz >= 2 then begin
       emit (Plhz(GPR0, Cint osrc, rsrc));
       emit (Psth(GPR0, Cint odst, rdst));
-      copy (Integers.Int.add osrc _2) (Integers.Int.add odst _2) (sz - 2)
+      copy (Int.add osrc _2) (Int.add odst _2) (sz - 2)
     end else if sz >= 1 then begin
       emit (Plbz(GPR0, Cint osrc, rsrc));
       emit (Pstb(GPR0, Cint odst, rdst));
-      copy (Integers.Int.add osrc _1) (Integers.Int.add odst _1) (sz - 1)
+      copy (Int.add osrc _1) (Int.add odst _1) (sz - 1)
     end in
   copy osrc odst sz
 
@@ -133,7 +134,7 @@ let memcpy_big_arg arg tmp =
   | BA (IR r) ->
       emit (Paddi(tmp, r, Cint _m4))
   | BA_addrstack ofs ->
-      emit_addimm tmp GPR1 (Integers.Int.add ofs _m4)
+      emit_addimm tmp GPR1 (Int.add ofs _m4)
   | _ ->
       assert false
 
@@ -226,10 +227,10 @@ let expand_volatile_access
 let offset_constant cst delta =
   match cst with
   | Cint n ->
-      let n' = Integers.Int.add n delta in
+      let n' = Int.add n delta in
       if offset_in_range n' then Some (Cint n') else None
   | Csymbol_sda(id, ofs) ->
-      Some (Csymbol_sda(id, Integers.Int.add ofs delta))
+      Some (Csymbol_sda(id, Int.add ofs delta))
   | _ -> None
 
 let expand_load_int64 hi lo base ofs_hi ofs_lo =
@@ -437,7 +438,7 @@ let expand_integer_cond_move a1 a2 a3 res =
   if a2 = a3 then
     emit (Pmr (res, a2))
   else if eref then begin
-    emit (Pcmpwi (a1,Cint (Integers.Int.zero)));
+    emit (Pcmpwi (a1,Cint (Int.zero)));
     emit (Pisel (res,a3,a2,CRbit_2))
   end else begin
     (* a1 has type _Bool, hence it is 0 or 1 *)
@@ -682,23 +683,23 @@ let expand_builtin_inline name args res =
   | "__builtin_icbi", [BA(IR a1)],_ ->
       emit (Picbi(GPR0,a1))
   | "__builtin_dcbtls", [BA (IR a1); BA_int loc],_ ->
-      if not ((Integers.Int.eq loc _0) || (Integers.Int.eq loc _2)) then
+      if not ((Int.eq loc _0) || (Int.eq loc _2)) then
         raise (Error "the second argument of __builtin_dcbtls must be 0 or 2");
       emit (Pdcbtls (loc,GPR0,a1))
   | "__builtin_dcbtls",_,_ ->
       raise (Error "the second argument of __builtin_dcbtls must be a constant")
   | "__builtin_icbtls", [BA (IR a1); BA_int loc],_ ->
-    if not ((Integers.Int.eq loc _0) || (Integers.Int.eq loc _2)) then
+    if not ((Int.eq loc _0) || (Int.eq loc _2)) then
         raise (Error "the second argument of __builtin_icbtls must be 0 or 2");
       emit (Picbtls (loc,GPR0,a1))
   | "__builtin_icbtls",_,_ ->
       raise (Error "the second argument of __builtin_icbtls must be a constant")
   | "__builtin_prefetch" , [BA (IR a1) ;BA_int rw; BA_int loc],_ ->
-      if not (Integers.Int.ltu loc _4) then
+      if not (Int.ltu loc _4) then
         raise (Error "the last argument of __builtin_prefetch must be 0, 1 or 2");
-      if Integers.Int.eq rw _0 then begin
+      if Int.eq rw _0 then begin
         emit (Pdcbt (loc,GPR0,a1));
-      end else if Integers.Int.eq rw _1 then begin
+      end else if Int.eq rw _1 then begin
         emit (Pdcbtst (loc,GPR0,a1));
       end else
         raise (Error "the second argument of __builtin_prefetch must be 0 or 1")