Code cleanup.

Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.

3 files changed, 49 insertions, 58 deletions

diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 75a629c5..dd7306fc 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -142,7 +142,7 @@ type instruction_arg =
   | Freg of freg
   | Constant of constant
   | Crbit of crbit
-  | Label of positive
+  | ALabel of positive
   | Float32 of Floats.float32
   | Float64 of Floats.float
   | Atom of positive
@@ -152,7 +152,7 @@ let p_arg oc = function
   | Freg fr -> p_freg oc fr
   | Constant c -> p_constant oc c
   | Crbit cr -> p_crbit oc cr
-  | Label lbl -> p_label oc lbl
+  | ALabel lbl -> p_label oc lbl
   | Float32 f -> p_float32_constant oc f
   | Float64 f  -> p_float64_constant oc f
   | Atom a -> p_atom_constant oc a
@@ -176,16 +176,16 @@ let p_instruction oc ic =
   | Pandc (ir1,ir2,ir3) -> instruction "Pandc" [Ireg ir1; Ireg ir2; Ireg ir3]
   | Pandi_ (ir1,ir2,c) -> instruction "Pandi_" [Ireg ir1; Ireg ir2; Constant c]
   | Pandis_ (ir1,ir2,c) -> instruction "Pandis_" [Ireg ir1; Ireg ir2; Constant c]
-  | Pb l -> instruction "Pb" [Label l]
-  | Pbctr s -> instruction "Pbctr" []
-  | Pbctrl s -> instruction "Pbctrl" []
-  | Pbdnz l -> instruction "Pbdnz" [Label l]
-  | Pbf (cr,l) -> instruction "Pbf" [Crbit cr; Label l]
-  | Pbl (i,s) -> instruction "Pbl" [Atom i]
-  | Pbs (i,s) -> instruction "Pbs" [Atom i]
+  | Pb l -> instruction "Pb" [ALabel l]
+  | Pbctr _ -> instruction "Pbctr" []
+  | Pbctrl _ -> instruction "Pbctrl" []
+  | Pbdnz l -> instruction "Pbdnz" [ALabel l]
+  | Pbf (cr,l) -> instruction "Pbf" [Crbit cr; ALabel l]
+  | Pbl (i,_) -> instruction "Pbl" [Atom i]
+  | Pbs (i,_) -> instruction "Pbs" [Atom i]
   | Pblr -> instruction "Pblr" []
-  | Pbt (cr,l) ->  instruction "Pbt" [Crbit cr; Label l]
-  | Pbtbl (i,lb) -> instruction "Pbtbl" ((Ireg i)::(List.map (fun a -> Label a) lb))
+  | Pbt (cr,l) ->  instruction "Pbt" [Crbit cr; ALabel l]
+  | Pbtbl (i,lb) -> instruction "Pbtbl" ((Ireg i)::(List.map (fun a -> ALabel a) lb))
   | Pcmpb (ir1,ir2,ir3) -> instruction "Pcmpb" [Ireg ir1; Ireg ir2; Ireg ir3]
   | Pcmplw (ir1,ir2) -> instruction "Pcmplw" [Ireg ir1; Ireg ir2]
   | Pcmplwi (ir,c) -> instruction "Pcmplwi" [Ireg ir; Constant c]
@@ -208,13 +208,13 @@ let p_instruction oc ic =
   | Pextsb (ir1,ir2) -> instruction "Pextsb" [Ireg ir1; Ireg ir2]
   | Pextsh (ir1,ir2) -> instruction "Pextsh" [Ireg ir1; Ireg ir2]
   | Pextsw (ir1,ir2) -> instruction "Pextsw" [Ireg ir1; Ireg ir2]
-  | Pfreeframe (c,i) -> assert false (* Should not occur *)
+  | Pfreeframe _ -> assert false (* Should not occur *)
   | Pfabs (fr1,fr2)
   | Pfabss (fr1,fr2) -> instruction "Pfabs" [Freg fr1; Freg fr2]
   | Pfadd (fr1,fr2,fr3) -> instruction "Pfadd" [Freg fr1; Freg fr2; Freg fr3]
   | Pfadds (fr1,fr2,fr3) -> instruction "Pfadds" [Freg fr1; Freg fr2; Freg fr3]
   | Pfcmpu (fr1,fr2) -> instruction "Pfcmpu" [Freg fr1; Freg fr2]
-  | Pfcfi (ir,fr) -> () (* Should not occur *)
+  | Pfcfi _ -> () (* Should not occur *)
   | Pfcfid (fr1,fr2) -> instruction "Pfcfid" [Freg fr1; Freg fr2]
   | Pfcfiu _ (* Should not occur *)
   | Pfcti _ (* Should not occur *)
@@ -224,14 +224,14 @@ let p_instruction oc ic =
   | Pfctiwz (fr1,fr2) -> instruction "Pfctiwz" [Freg fr1; Freg fr2]
   | Pfdiv (fr1,fr2,fr3) -> instruction "Pfdiv" [Freg fr1; Freg fr2; Freg fr3]
   | Pfdivs (fr1,fr2,fr3) -> instruction "Pfdivs" [Freg fr1; Freg fr2; Freg fr3]
-  | Pfmake (fr,ir1,ir2) -> ()(* Should not occur *)
+  | Pfmake _ -> ()(* Should not occur *)
   | Pfmr (fr1,fr2) -> instruction "Pfmr" [Freg fr1; Freg fr2]
   | Pfmul (fr1,fr2,fr3) -> instruction "Pfmul" [Freg fr1; Freg fr2; Freg fr3]
   | Pfmuls(fr1,fr2,fr3) -> instruction "Pfmuls" [Freg fr1; Freg fr2; Freg fr3]
   | Pfneg (fr1,fr2)
   | Pfnegs (fr1,fr2) -> instruction "Pfneg" [Freg fr1; Freg fr2]
   | Pfrsp (fr1,fr2) -> instruction "Pfrsp" [Freg fr1; Freg fr2]
-  | Pfxdp (fr1,fr2) -> () (* Should not occur *)
+  | Pfxdp _ -> () (* Should not occur *)
   | Pfsub (fr1,fr2,fr3) -> instruction "Pfsub" [Freg fr1; Freg fr2; Freg fr3]
   | Pfsubs (fr1,fr2,fr3) ->  instruction "Pfsubs" [Freg fr1; Freg fr2; Freg fr3]
   | Pfmadd (fr1,fr2,fr3,fr4) -> instruction "Pfmadd" [Freg fr1; Freg fr2; Freg fr3; Freg fr4]
@@ -271,7 +271,7 @@ let p_instruction oc ic =
   | Plwbrx (ir1,ir2,ir3) -> instruction "Plwbrx" [Ireg ir1; Ireg ir2; Ireg ir3]
   | Pmbar c -> instruction "Pmbar" [Constant (Cint c)]
   | Pmfcr ir -> instruction "Pmfcr" [Ireg ir]
-  | Pmfcrbit (ir,crb) -> () (* Should not occur *)
+  | Pmfcrbit _ -> () (* Should not occur *)
   | Pmflr ir -> instruction "Pmflr" [Ireg ir]
   | Pmr (ir1,ir2) -> instruction "Pmr" [Ireg ir1; Ireg ir2]
   | Pmtctr ir -> instruction "Pmtctr" [Ireg ir]
@@ -326,7 +326,7 @@ let p_instruction oc ic =
   | Pxor (ir1,ir2,ir3) -> instruction "Pxor" [Ireg ir1; Ireg ir2; Ireg ir3]
   | Pxori (ir1,ir2,c) ->instruction "Pxori" [Ireg ir1; Ireg ir2; Constant c]
   | Pxoris (ir1,ir2,c) -> instruction "Pxoris" [Ireg ir1; Ireg ir2; Constant c]
-  | Plabel l -> instruction "Plabel" [Label l]
+  | Plabel l -> instruction "Plabel" [ALabel l]
   | Pbuiltin _ -> ()
   | Pcfi_adjust _  (* Only debug relevant *)
   | Pcfi_rel_offset _ ->  () (* Only debug relevant *) in
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 7af27d20..a6795030 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -13,11 +13,9 @@
 (* Expanding built-ins and some pseudo-instructions by rewriting
    of the PPC assembly code. *)
 
-open Datatypes
 open Camlcoq
 open Integers
 open AST
-open Memdata
 open Asm
 open Asmexpandaux
 
@@ -122,7 +120,7 @@ let memcpy_big_arg arg tmp =
   | _ ->
       assert false
 
-let expand_builtin_memcpy_big sz al src dst =
+let expand_builtin_memcpy_big sz _ src dst =
   assert (sz >= 4);
   emit_loadimm GPR0 (Z.of_uint (sz / 4));
   emit (Pmtctr GPR0);
@@ -723,7 +721,7 @@ let expand_instruction instr =
       emit (Prlwinm(r1, r1, Z.of_uint (1 + num_crbit bit), _1))
   | Pbuiltin(ef, args, res) ->
       begin match ef with
-      | EF_builtin(name, sg) ->
+      | EF_builtin(name, _) ->
           expand_builtin_inline (camlstring_of_coqstring name) args res
       | EF_vload chunk ->
           expand_builtin_vload chunk args res
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 3d183972..93d73d5c 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -14,12 +14,11 @@
 
 open Printf
 open Fileinfo
-open Datatypes
+open !Datatypes
 open Maps
 open Camlcoq
 open Sections
 open AST
-open Memdata
 open Asm
 open PrintAsmaux
 
@@ -230,7 +229,7 @@ module Diab_System : SYSTEM =
       let name = name_of_section sec in
       assert (name <> "COMM");
       match sec with
-      | Section_debug_info (Some s) ->
+      | Section_debug_info (Some _) ->
           fprintf oc "	%s\n" name;
           fprintf oc "	.sectionlink	.debug_info\n"
       | _ ->
@@ -240,13 +239,13 @@ module Diab_System : SYSTEM =
       print_file_line_d2 oc comment file line
 
     (* Emit .cfi directives *)
-    let cfi_startproc oc = ()
+    let cfi_startproc _ = ()
 
-    let cfi_endproc oc = ()
+    let cfi_endproc _ = ()
 
-    let cfi_adjust oc delta = ()
+    let cfi_adjust _ _ = ()
 
-    let cfi_rel_offset oc reg ofs = ()
+    let cfi_rel_offset _ _ _ = ()
 
     let debug_section oc sec =
       match sec with
@@ -303,9 +302,6 @@ module Target (System : SYSTEM):TARGET =
     (* Basic printing functions *)
     let symbol = symbol
 
-    let raw_symbol oc s =
-      fprintf oc "%s" s
-
     let label = label
 
     let label_low oc lbl =
@@ -340,9 +336,6 @@ module Target (System : SYSTEM):TARGET =
       | FR r -> fprintf oc "f%s" (float_reg_name r)
       | _    -> assert false
 
-    let print_location oc loc =
-      if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
-
     (* Encoding masks for rlwinm instructions *)
 
     let rolm_mask n =
@@ -387,7 +380,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	addis	%a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c
       | Paddze(r1, r2) ->
           fprintf oc "	addze	%a, %a\n" ireg r1 ireg r2
-      | Pallocframe(sz, ofs, _) ->
+      | Pallocframe _ ->
           assert false
       | Pand_(r1, r2, r3) ->
           fprintf oc "	and.	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
@@ -399,9 +392,9 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	andis.	%a, %a, %a\n" ireg r1 ireg r2 constant c
       | Pb lbl ->
           fprintf oc "	b	%a\n" label (transl_label lbl)
-      | Pbctr sg ->
+      | Pbctr _ ->
           fprintf oc "	bctr\n"
-      | Pbctrl sg ->
+      | Pbctrl _ ->
           fprintf oc "	bctrl\n"
       | Pbdnz lbl ->
           fprintf oc "	bdnz	%a\n" label (transl_label lbl)
@@ -416,9 +409,9 @@ module Target (System : SYSTEM):TARGET =
             fprintf oc "	b	%a\n" label (transl_label lbl);
             fprintf oc "%a:\n" label next
           end
-      | Pbl(s, sg) ->
+      | Pbl(s, _) ->
           fprintf oc "	bl	%a\n" symbol s
-      | Pbs(s, sg) ->
+      | Pbs(s, _) ->
           fprintf oc "	b	%a\n" symbol s
       | Pblr ->
           fprintf oc "	blr\n"
@@ -490,7 +483,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	extsh	%a, %a\n" ireg r1 ireg r2
       | Pextsw(r1, r2) ->
           fprintf oc "	extsw	%a, %a\n" ireg r1 ireg r2
-      | Pfreeframe(sz, ofs) ->
+      | Pfreeframe _ ->
           assert false
       | Pfabs(r1, r2) | Pfabss(r1, r2) ->
           fprintf oc "	fabs	%a, %a\n" freg r1 freg r2
@@ -500,17 +493,17 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fadds	%a, %a, %a\n" freg r1 freg r2 freg r3
       | Pfcmpu(r1, r2) ->
           fprintf oc "	fcmpu	%a, %a, %a\n" creg 0 freg r1 freg r2
-      | Pfcfi(r1, r2) ->
+      | Pfcfi _ ->
           assert false
       | Pfcfid(r1, r2) ->
           fprintf oc "	fcfid	%a, %a\n" freg r1 freg r2
-      | Pfcfiu(r1, r2) ->
+      | Pfcfiu _ ->
           assert false
-      | Pfcti(r1, r2) ->
+      | Pfcti _ ->
           assert false
       | Pfctidz(r1, r2) ->
           fprintf oc "	fctidz	%a, %a\n" freg r1 freg r2
-      | Pfctiu(r1, r2) ->
+      | Pfctiu _ ->
           assert false
       | Pfctiw(r1, r2) ->
           fprintf oc "	fctiw	%a, %a\n" freg r1 freg r2
@@ -520,7 +513,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fdiv	%a, %a, %a\n" freg r1 freg r2 freg r3
       | Pfdivs(r1, r2, r3) ->
           fprintf oc "	fdivs	%a, %a, %a\n" freg r1 freg r2 freg r3
-      | Pfmake(rd, r1, r2) ->
+      | Pfmake _ ->
           assert false
       | Pfmr(r1, r2) ->
           fprintf oc "	fmr	%a, %a\n" freg r1 freg r2
@@ -532,7 +525,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fneg	%a, %a\n" freg r1 freg r2
       | Pfrsp(r1, r2) ->
           fprintf oc "	frsp	%a, %a\n" freg r1 freg r2
-      | Pfxdp(r1, r2) ->
+      | Pfxdp _ ->
           assert false
       | Pfsub(r1, r2, r3) ->
           fprintf oc "	fsub	%a, %a, %a\n" freg r1 freg r2 freg r3
@@ -610,7 +603,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	mbar	%ld\n" (camlint_of_coqint mo)
       | Pmfcr(r1) ->
           fprintf oc "	mfcr	%a\n" ireg r1
-      | Pmfcrbit(r1, bit) ->
+      | Pmfcrbit _ ->
           assert false
       | Pmflr(r1) ->
           fprintf oc "	mflr	%a\n" ireg r1
@@ -726,13 +719,13 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "%a:\n" label (transl_label lbl)
       | Pbuiltin(ef, args, res) ->
           begin match ef with
-          | EF_annot(txt, targs) ->
+          | EF_annot(txt, _) ->
               fprintf oc "%s annotation: " comment;
               print_annot_text preg_annot "r1" oc (camlstring_of_coqstring txt) args
-          | EF_debug(kind, txt, targs) ->
+          | EF_debug(kind, txt, _) ->
               print_debug_info comment print_file_line preg_annot "r1" oc
                                (P.to_int kind) (extern_atom txt) args
-          | EF_inline_asm(txt, sg, clob) ->
+          | EF_inline_asm(txt, sg, _) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
               print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
@@ -757,14 +750,14 @@ module Target (System : SYSTEM):TARGET =
        PowerPC instructions.  We can over-approximate. *)
 
     let instr_size = function
-      | Pbf(bit, lbl) -> 2
-      | Pbt(bit, lbl) -> 2
-      | Pbtbl(r, tbl) -> 5
-      | Plfi(r1, c) -> 2
-      | Plfis(r1, c) -> 2
-      | Plabel lbl -> 0
-      | Pbuiltin((EF_annot _ | EF_debug _), args, res) -> 0
-      | Pbuiltin(ef, args, res) -> 3
+      | Pbf _ -> 2
+      | Pbt _ -> 2
+      | Pbtbl _ -> 5
+      | Plfi _ -> 2
+      | Plfis _ -> 2
+      | Plabel _-> 0
+      | Pbuiltin ((EF_annot _ | EF_debug _), _, _) -> 0
+      | Pbuiltin _ -> 3
       | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0
       | _ -> 1