diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-10 13:35:48 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-10 13:35:48 +0100 |
commit | 5b05d3668571bd9b748b781b0cc29ae10f745f61 (patch) | |
tree | aa235b80ff0666c34332be46664ae289d8afaa2c | |
parent | 272087e1bc62bead1d1e1bea3d64e12d013eea37 (diff) | |
download | compcert-5b05d3668571bd9b748b781b0cc29ae10f745f61.tar.gz compcert-5b05d3668571bd9b748b781b0cc29ae10f745f61.zip |
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.
56 files changed, 590 insertions, 740 deletions
diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll index 6695b6b7..82769924 100644 --- a/backend/CMlexer.mll +++ b/backend/CMlexer.mll @@ -14,8 +14,6 @@ (* *********************************************************************) { -open BinNums -open Camlcoq open CMparser exception Error of string } diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 5f189e7b..b20dea38 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -17,7 +17,7 @@ including function calls in expressions, matches, while statements, etc. */ %{ -open Datatypes +open !Datatypes open Camlcoq open BinNums open Integers @@ -210,17 +210,17 @@ let mkmatch_aux expr cases = let ncases = List.length cases in let rec mktable n = function | [] -> assert false - | [key, action] -> [] - | (key, action) :: rem -> + | [_, _] -> [] + | (key, _) :: rem -> (coqint_of_camlint key, Nat.of_int n) :: mktable (n + 1) rem in let sw = Sswitch(false, expr, mktable 0 cases, Nat.of_int (ncases - 1)) in let rec mkblocks body n = function | [] -> assert false - | [key, action] -> + | [_, action] -> Sblock(Sseq(body, action)) - | (key, action) :: rem -> + | (_, action) :: rem -> mkblocks (Sblock(Sseq(body, Sseq(action, Sexit (Nat.of_int n))))) (n - 1) @@ -233,7 +233,7 @@ let mkmatch expr cases = let s = match cases with | [] -> Sskip (* ??? *) - | [key, action] -> action + | [_, action] -> action | _ -> mkmatch_aux c cases in prepend_seq !convert_accu s diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index 72bf9cb4..399eb9bd 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -18,11 +18,9 @@ (* FIXME: proper support for type Tsingle *) open Printf -open Datatypes open Camlcoq open AST open PrintAST -open Integers open Cminor exception Error of string @@ -74,21 +72,6 @@ let type_var env id = with Not_found -> raise (Error (sprintf "Unbound variable %s\n" (extern_atom id))) -let type_letvar env n = - let n = Nat.to_int n in - try - List.nth env n - with Not_found -> - raise (Error (sprintf "Unbound let variable #%d\n" n)) - -let name_of_comparison = function - | Ceq -> "eq" - | Cne -> "ne" - | Clt -> "lt" - | Cle -> "le" - | Cgt -> "gt" - | Cge -> "ge" - let type_constant = function | Ointconst _ -> tint | Ofloatconst _ -> tfloat @@ -313,12 +296,12 @@ let rec type_stmt env blk ret s = | Sexit n -> if Nat.to_int n >= blk then raise (Error (sprintf "Bad exit(%d)\n" (Nat.to_int n))) - | Sswitch(islong, e, cases, deflt) -> + | Sswitch(islong, e, _, _) -> unify (type_expr env [] e) (if islong then tlong else tint) | Sreturn None -> begin match ret with | None -> () - | Some tret -> raise (Error ("return without argument")) + | Some _ -> raise (Error ("return without argument")) end | Sreturn (Some e) -> begin match ret with @@ -339,9 +322,9 @@ let rec type_stmt env blk ret s = with Error s -> raise (Error (sprintf "In tail call:\n%s" s)) end - | Slabel(lbl, s1) -> + | Slabel(_, s1) -> type_stmt env blk ret s1 - | Sgoto lbl -> + | Sgoto _ -> () let rec env_of_vars idl = @@ -360,8 +343,8 @@ let type_function id f = let type_globdef (id, gd) = match gd with | Gfun(Internal f) -> type_function id f - | Gfun(External ef) -> () - | Gvar v -> () + | Gfun(External _) -> () + | Gvar _ -> () let type_program p = List.iter type_globdef p.prog_defs; p diff --git a/backend/Fileinfo.ml b/backend/Fileinfo.ml index 0490def0..a78a24db 100644 --- a/backend/Fileinfo.ml +++ b/backend/Fileinfo.ml @@ -25,7 +25,7 @@ let reset_filenames () = let close_filenames () = Hashtbl.iter - (fun file (num, fb) -> + (fun _ (_, fb) -> match fb with Some b -> Printlines.close b | None -> ()) filename_info; reset_filenames() @@ -46,7 +46,7 @@ let print_file oc file = try Hashtbl.find filename_info file with Not_found -> - let (filenum, filebuf as res) = enter_filename file in + let (filenum, _ as res) = enter_filename file in fprintf oc " .file %d %S\n" filenum file; res diff --git a/backend/IRC.ml b/backend/IRC.ml index eb677069..8780bce3 100644 --- a/backend/IRC.ml +++ b/backend/IRC.ml @@ -12,13 +12,11 @@ open Printf open Camlcoq -open Datatypes open AST open Registers open Machregs open Locations open Conventions1 -open Conventions open XTL (* Iterated Register Coalescing: George and Appel's graph coloring algorithm *) @@ -116,7 +114,7 @@ let name_of_loc = function let name_of_node n = match n.var with - | V(r, ty) -> sprintf "x%ld" (P.to_int32 r) + | V(r, _) -> sprintf "x%ld" (P.to_int32 r) | L l -> name_of_loc l (* The algorithm manipulates partitions of the nodes and of the moves @@ -138,7 +136,6 @@ module DLinkNode = struct nstate = state; nprev = empty; nnext = empty } in empty let dummy = make Colored - let clear dl = dl.nnext <- dl; dl.nprev <- dl let notempty dl = dl.nnext != dl let insert n dl = n.nstate <- dl.nstate; @@ -167,7 +164,6 @@ module DLinkMove = struct mstate = state; mprev = empty; mnext = empty } in empty let dummy = make CoalescedMoves - let clear dl = dl.mnext <- dl; dl.mprev <- dl let notempty dl = dl.mnext != dl let insert m dl = m.mstate <- dl.mstate; @@ -180,12 +176,6 @@ module DLinkMove = struct remove m dl1; insert m dl2 let pick dl = let m = dl.mnext in remove m dl; m - let iter f dl = - let rec iter m = if m != dl then (f m; iter m.mnext) - in iter dl.mnext - let fold f dl accu = - let rec fold m accu = if m == dl then accu else fold m.mnext (f m accu) - in fold dl.mnext accu end (* Auxiliary data structures *) @@ -447,7 +437,7 @@ let moveRelated n = (* Initial partition of nodes into spill / freeze / simplify *) let initialNodePartition g = - let part_node v n = + let part_node n = match n.nstate with | Initial -> let k = g.num_available_registers.(n.regclass) in @@ -459,44 +449,7 @@ let initialNodePartition g = DLinkNode.insert n g.simplifyWorklist | Colored -> () | _ -> assert false in - Hashtbl.iter part_node g.varTable - - -(* Check invariants *) - -let degreeInvariant g n = - let c = ref 0 in - iterAdjacent (fun n -> incr c) n; - if !c <> n.degree then - failwith("degree invariant violated by " ^ name_of_node n) - -let simplifyWorklistInvariant g n = - if n.degree < g.num_available_registers.(n.regclass) - && not (moveRelated n) - then () - else failwith("simplify worklist invariant violated by " ^ name_of_node n) - -let freezeWorklistInvariant g n = - if n.degree < g.num_available_registers.(n.regclass) - && moveRelated n - then () - else failwith("freeze worklist invariant violated by " ^ name_of_node n) - -let spillWorklistInvariant g n = - if n.degree >= g.num_available_registers.(n.regclass) - then () - else failwith("spill worklist invariant violated by " ^ name_of_node n) - -let checkInvariants g = - DLinkNode.iter - (fun n -> degreeInvariant g n; simplifyWorklistInvariant g n) - g.simplifyWorklist; - DLinkNode.iter - (fun n -> degreeInvariant g n; freezeWorklistInvariant g n) - g.freezeWorklist; - DLinkNode.iter - (fun n -> degreeInvariant g n; spillWorklistInvariant g n) - g.spillWorklist + Hashtbl.iter (fun _ a -> part_node a) g.varTable (* Enable moves that have become low-degree related *) @@ -737,7 +690,7 @@ let selectSpill g = (* Find a spillable node of minimal cost *) let (n, cost) = DLinkNode.fold - (fun n (best_node, best_cost as best) -> + (fun n (_, best_cost as best) -> (* Manual inlining of [spillCost] above plus algebraic simplif *) let deg = float n.degree in let deg2 = deg *. deg in @@ -894,7 +847,7 @@ let assign_color g n = let location_of_var g v = match v with | L l -> l - | V(r, ty) -> + | V(_, ty) -> try let n = Hashtbl.find g.varTable v in let n' = getAlias n in diff --git a/backend/IRC.mli b/backend/IRC.mli index e81b6dc5..d27dedaa 100644 --- a/backend/IRC.mli +++ b/backend/IRC.mli @@ -12,7 +12,6 @@ (* Iterated Register Coalescing: George and Appel's graph coloring algorithm *) -open AST open Registers open Machregs open Locations diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml index 42129166..7893da89 100644 --- a/backend/Inliningaux.ml +++ b/backend/Inliningaux.ml @@ -10,9 +10,7 @@ (* *) (* *********************************************************************) -open Camlcoq - (* To be considered: heuristics based on size of function? *) -let should_inline (id: AST.ident) (f: RTL.coq_function) = +let should_inline (id: AST.ident) (_: RTL.coq_function) = C2C.atom_is_inline id diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 71ee2e56..41a98873 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -10,10 +10,7 @@ (* *) (* *********************************************************************) -open Coqlib -open Datatypes open LTL -open Lattice open Maps open Camlcoq @@ -82,13 +79,13 @@ let basic_blocks f joins = let rec do_instr_list = function | [] -> assert false | Lbranch s :: _ -> next_in_block blk minpc s - | Ltailcall (sig0, ros) :: _ -> end_block blk minpc - | Lcond (cond, args, ifso, ifnot) :: _ -> + | Ltailcall _ :: _ -> end_block blk minpc + | Lcond (_, _, ifso, ifnot) :: _ -> end_block blk minpc; start_block ifso; start_block ifnot - | Ljumptable(arg, tbl) :: _ -> + | Ljumptable(_, tbl) :: _ -> end_block blk minpc; List.iter start_block tbl | Lreturn :: _ -> end_block blk minpc - | instr :: b' -> do_instr_list b' in + | _ :: b' -> do_instr_list b' in do_instr_list b (* next_in_block: check if join point and either extend block or start block *) @@ -113,5 +110,5 @@ let flatten_blocks blks = (* Build the enumeration *) -let enumerate_aux f reach = +let enumerate_aux f _ = flatten_blocks (basic_blocks f (join_points f)) diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 6c1eda57..6eff7c02 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -12,9 +12,8 @@ (* *********************************************************************) open AST -open Asm open Camlcoq -open Datatypes +open !Datatypes open DwarfPrinter open PrintAsmaux open Printf @@ -105,7 +104,7 @@ module Printer(Target:TARGET) = let print_globdef oc (name,gdef) = match gdef with | Gfun (Internal code) -> print_function oc name code - | Gfun (External ef) -> () + | Gfun (External _) -> () | Gvar v -> print_var oc name v module DwarfTarget: DwarfTypes.DWARF_TARGET = @@ -119,7 +118,7 @@ module Printer(Target:TARGET) = module DebugPrinter = DwarfPrinter (DwarfTarget) end -let print_program oc p db = +let print_program oc p = let module Target = (val (sel_target ()):TARGET) in let module Printer = Printer(Target) in Fileinfo.reset_filenames (); diff --git a/backend/PrintAsm.mli b/backend/PrintAsm.mli index 0b2869b0..29e91540 100644 --- a/backend/PrintAsm.mli +++ b/backend/PrintAsm.mli @@ -11,4 +11,4 @@ (* *) (* *********************************************************************) -val print_program: out_channel -> Asm.program -> DwarfTypes.dw_entry option -> unit +val print_program: out_channel -> Asm.program -> unit diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 0ca5b8e0..148c5300 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -14,7 +14,6 @@ open AST open Asm open Camlcoq -open Datatypes open Memdata open Printf open Sections diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 9b6b1488..5e686b55 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -17,7 +17,6 @@ open Format open Camlcoq -open Datatypes open Integers open AST open PrintAST @@ -27,7 +26,7 @@ open Cminor type associativity = LtoR | RtoL | NA -let rec precedence = function +let precedence = function | Evar _ -> (16, NA) | Econst _ -> (16, NA) | Eunop _ -> (15, RtoL) diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index 0f78bc58..ba28b30d 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -17,8 +17,7 @@ open Camlcoq open Datatypes open Maps open AST -open Integers -open Locations +open !Locations open LTL open PrintAST open PrintOp @@ -73,9 +72,9 @@ let print_instruction pp succ = function | Lstore(chunk, addr, args, src) -> fprintf pp "%s[%a] = %a" (name_of_chunk chunk) (print_addressing mreg) (addr, args) mreg src - | Lcall(sg, fn) -> + | Lcall(_, fn) -> fprintf pp "call %a" ros fn - | Ltailcall(sg, fn) -> + | Ltailcall(_, fn) -> fprintf pp "tailcall %a" ros fn | Lbuiltin(ef, args, res) -> fprintf pp "%a = %s(%a)" diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml index 0ce2e87b..07ec6a1a 100644 --- a/backend/PrintMach.ml +++ b/backend/PrintMach.ml @@ -15,14 +15,10 @@ open Printf open Camlcoq open Datatypes -open Maps open AST -open Integers -open Locations open Machregsaux open Mach open PrintAST -open PrintOp let reg pp r = match name_of_register r with @@ -61,9 +57,9 @@ let print_instruction pp i = (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) reg src - | Mcall(sg, fn) -> + | Mcall(_, fn) -> fprintf pp "\tcall %a\n" ros fn - | Mtailcall(sg, fn) -> + | Mtailcall(_, fn) -> fprintf pp "\ttailcall %a\n" ros fn | Mbuiltin(ef, args, res) -> fprintf pp "\t%a = %s(%a)\n" diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index f2242c13..a22aa422 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -17,10 +17,8 @@ open Camlcoq open Datatypes open Maps open AST -open Integers open RTL open PrintAST -open PrintOp (* Printing of RTL code *) @@ -63,11 +61,11 @@ let print_instruction pp (pc, i) = (PrintOp.print_addressing reg) (addr, args) reg src; print_succ pp s (pc - 1) - | Icall(sg, fn, args, res, s) -> + | Icall(_, fn, args, res, s) -> fprintf pp "%a = %a(%a)\n" reg res ros fn regs args; print_succ pp s (pc - 1) - | Itailcall(sg, fn, args) -> + | Itailcall(_, fn, args) -> fprintf pp "tailcall %a(%a)\n" ros fn regs args | Ibuiltin(ef, args, res, s) -> diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml index dd8434da..1bee1e15 100644 --- a/backend/PrintXTL.ml +++ b/backend/PrintXTL.ml @@ -17,9 +17,7 @@ open Camlcoq open Datatypes open Maps open AST -open Registers -open Op -open Locations +open !Locations open PrintAST open PrintOp open XTL @@ -69,8 +67,8 @@ let ros pp = function let liveset pp lv = fprintf pp "{"; - VSet.iter (function V(r, ty) -> fprintf pp " x%d" (P.to_int r) - | L l -> ()) + VSet.iter (function V(r, _) -> fprintf pp " x%d" (P.to_int r) + | L _ -> ()) lv; fprintf pp " }" @@ -95,9 +93,9 @@ let print_instruction pp succ = function | Xstore(chunk, addr, args, src) -> fprintf pp "%s[%a] = %a" (name_of_chunk chunk) (print_addressing var) (addr, args) var src - | Xcall(sg, fn, args, res) -> + | Xcall(_, fn, args, res) -> fprintf pp "%a = call %a(%a)" vars res ros fn vars args - | Xtailcall(sg, fn, args) -> + | Xtailcall(_, fn, args) -> fprintf pp "tailcall %a(%a)" ros fn vars args | Xbuiltin(ef, args, res) -> fprintf pp "%a = %s(%a)" diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index 045299d4..fdf41897 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -11,9 +11,7 @@ (* *********************************************************************) open Datatypes -open Camlcoq open AST -open Switch open CminorSel (* Heuristic to orient if-then-else statements. @@ -28,22 +26,22 @@ open CminorSel putting the bigger of the two branches in fall-through position. *) let rec size_expr = function - | Evar id -> 0 - | Eop(op, args) -> 1 + size_exprs args - | Eload(chunk, addr, args) -> 1 + size_exprs args + | Evar _ -> 0 + | Eop(_, args) -> 1 + size_exprs args + | Eload(_, _, args) -> 1 + size_exprs args | Econdition(ce, e1, e2) -> 1 + size_condexpr ce + max (size_expr e1) (size_expr e2) | Elet(e1, e2) -> size_expr e1 + size_expr e2 - | Eletvar n -> 0 - | Ebuiltin(ef, el) -> 2 + size_exprs el - | Eexternal(id, sg, el) -> 5 + size_exprs el + | Eletvar _ -> 0 + | Ebuiltin(_, el) -> 2 + size_exprs el + | Eexternal(_, _, el) -> 5 + size_exprs el and size_exprs = function | Enil -> 0 | Econs(e1, el) -> size_expr e1 + size_exprs el and size_condexpr = function - | CEcond(c, args) -> size_exprs args + | CEcond(_, args) -> size_exprs args | CEcondition(c1, c2, c3) -> 1 + size_condexpr c1 + size_condexpr c2 + size_condexpr c3 | CElet(a, c) -> @@ -54,8 +52,8 @@ let size_exprlist al = List.fold_right (fun a s -> size_expr a + s) al 0 let size_builtin_args al = size_exprlist (params_of_builtin_args al) let rec size_exitexpr = function - | XEexit n -> 0 - | XEjumptable(arg, tbl) -> 2 + size_expr arg + | XEexit _ -> 0 + | XEjumptable(arg, _) -> 2 + size_expr arg | XEcondition(c1, c2, c3) -> 1 + size_condexpr c1 + size_exitexpr c2 + size_exitexpr c3 | XElet(a, c) -> @@ -63,34 +61,34 @@ let rec size_exitexpr = function let rec length_exprs = function | Enil -> 0 - | Econs(e1, el) -> 1 + length_exprs el + | Econs(_, el) -> 1 + length_exprs el let size_eos = function | Coq_inl e -> size_expr e - | Coq_inr id -> 0 + | Coq_inr _ -> 0 let rec size_stmt = function | Sskip -> 0 - | Sassign(id, a) -> size_expr a - | Sstore(chunk, addr, args, src) -> 1 + size_exprs args + size_expr src - | Scall(optid, sg, eos, args) -> + | Sassign(_, a) -> size_expr a + | Sstore(_, _, args, src) -> 1 + size_exprs args + size_expr src + | Scall(_, _, eos, args) -> 3 + size_eos eos + size_exprs args + length_exprs args - | Stailcall(sg, eos, args) -> + | Stailcall(_, eos, args) -> 3 + size_eos eos + size_exprs args + length_exprs args | Sbuiltin(_, (EF_annot _ | EF_debug _), _) -> 0 - | Sbuiltin(optid, ef, args) -> 1 + size_builtin_args args + | Sbuiltin(_, _, args) -> 1 + size_builtin_args args | Sseq(s1, s2) -> size_stmt s1 + size_stmt s2 | Sifthenelse(ce, s1, s2) -> size_condexpr ce + max (size_stmt s1) (size_stmt s2) | Sloop s -> 1 + 4 * size_stmt s | Sblock s -> size_stmt s - | Sexit n -> 1 + | Sexit _ -> 1 | Sswitch xe -> size_exitexpr xe | Sreturn None -> 2 | Sreturn (Some arg) -> 2 + size_expr arg - | Slabel(lbl, s) -> size_stmt s - | Sgoto lbl -> 1 + | Slabel(_, s) -> size_stmt s + | Sgoto _ -> 1 -let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = +let more_likely (_: condexpr) (ifso: stmt) (ifnot: stmt) = size_stmt ifso > size_stmt ifnot diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index a5fa8cd7..ee35d7a0 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -33,9 +33,7 @@ open Datatypes open Coqlib open Maps open AST -open Memdata open Kildall -open Registers open Op open Machregs open Locations @@ -87,16 +85,16 @@ let constrain_reg v c = let rec constrain_regs vl cl = match vl, cl with | [], _ -> [] - | v1 :: vl', [] -> vl - | v1 :: vl', Some mr1 :: cl' -> L(R mr1) :: constrain_regs vl' cl' + | _ :: _, [] -> vl + | _ :: vl', Some mr1 :: cl' -> L(R mr1) :: constrain_regs vl' cl' | v1 :: vl', None :: cl' -> v1 :: constrain_regs vl' cl' let move v1 v2 k = if v1 = v2 then k - else if is_stack_reg v1 then begin + else if XTL.is_stack_reg v1 then begin let t = new_temp (typeof v2) in Xmove(v1, t) :: Xmove(t, v2) :: k - end else if is_stack_reg v2 then begin + end else if XTL.is_stack_reg v2 then begin let t = new_temp (typeof v1) in Xmove(v1, t) :: Xmove(t, v2) :: k end else Xmove(v1, v2) :: k @@ -142,8 +140,8 @@ let convert_builtin_res tyenv = function let rec constrain_builtin_arg a cl = match a, cl with - | BA x, None :: cl' -> (a, cl') - | BA x, Some mr :: cl' -> (BA (L(R mr)), cl') + | BA _, None :: cl' -> (a, cl') + | BA _, Some mr :: cl' -> (BA (L(R mr)), cl') | BA_splitlong(hi, lo), _ -> let (hi', cl1) = constrain_builtin_arg hi cl in let (lo', cl2) = constrain_builtin_arg lo cl1 in @@ -160,8 +158,8 @@ let rec constrain_builtin_args al cl = let rec constrain_builtin_res a cl = match a, cl with - | BR x, None :: cl' -> (a, cl') - | BR x, Some mr :: cl' -> (BR (L(R mr)), cl') + | BR _, None :: cl' -> (a, cl') + | BR _, Some mr :: cl' -> (BR (L(R mr)), cl') | BR_splitlong(hi, lo), _ -> let (hi', cl1) = constrain_builtin_res hi cl in let (lo', cl2) = constrain_builtin_res lo cl1 in @@ -264,7 +262,7 @@ let block_of_RTL_instr funsig tyenv = function let next_pc f = PTree.fold - (fun npc pc i -> if P.lt pc npc then npc else P.succ pc) + (fun npc pc _ -> if P.lt pc npc then npc else P.succ pc) f.RTL.fn_code P.one (* Translate an RTL function to an XTL function *) @@ -289,7 +287,7 @@ let vset_removelist vl after = List.fold_right VSet.remove vl after let vset_addlist vl after = List.fold_right VSet.add vl after let vset_addros vos after = - match vos with Coq_inl v -> VSet.add v after | Coq_inr id -> after + match vos with Coq_inl v -> VSet.add v after | Coq_inr _ -> after let rec vset_addarg a after = match a with @@ -308,34 +306,34 @@ let rec vset_removeres r after = let live_before instr after = match instr with | Xmove(src, dst) | Xspill(src, dst) | Xreload(src, dst) -> - if VSet.mem dst after || is_stack_reg src + if VSet.mem dst after || XTL.is_stack_reg src then VSet.add src (VSet.remove dst after) else after - | Xparmove(srcs, dsts, itmp, ftmp) -> + | Xparmove(srcs, dsts, _, _) -> vset_addlist srcs (vset_removelist dsts after) - | Xop(op, args, res) -> + | Xop(_, args, res) -> if VSet.mem res after then vset_addlist args (VSet.remove res after) else after - | Xload(chunk, addr, args, dst) -> + | Xload(_, _, args, dst) -> if VSet.mem dst after then vset_addlist args (VSet.remove dst after) else after - | Xstore(chunk, addr, args, src) -> + | Xstore(_, _, args, src) -> vset_addlist args (VSet.add src after) - | Xcall(sg, ros, args, res) -> + | Xcall(_, ros, args, res) -> vset_addlist args (vset_addros ros (vset_removelist res after)) - | Xtailcall(sg, ros, args) -> + | Xtailcall(_, ros, args) -> vset_addlist args (vset_addros ros VSet.empty) - | Xbuiltin(EF_debug _, args, res) -> + | Xbuiltin(EF_debug _, _, res) -> vset_removeres res after - | Xbuiltin(ef, args, res) -> + | Xbuiltin(_, args, res) -> vset_addargs args (vset_removeres res after) - | Xbranch s -> + | Xbranch _ -> after - | Xcond(cond, args, s1, s2) -> + | Xcond(_, args, _, _) -> List.fold_right VSet.add args after - | Xjumptable(arg, tbl) -> + | Xjumptable(arg, _) -> VSet.add arg after | Xreturn args -> vset_addlist args VSet.empty @@ -385,7 +383,7 @@ let rec dce_parmove srcs dsts after = | [], [] -> [], [] | src1 :: srcs, dst1 :: dsts -> let (srcs', dsts') = dce_parmove srcs dsts after in - if VSet.mem dst1 after || is_stack_reg src1 + if VSet.mem dst1 after || XTL.is_stack_reg src1 then (src1 :: srcs', dst1 :: dsts') else (srcs', dsts') | _, _ -> assert false @@ -399,7 +397,7 @@ let rec keep_builtin_arg after = function let dce_instr instr after k = match instr with | Xmove(src, dst) -> - if VSet.mem dst after || is_stack_reg src + if VSet.mem dst after || XTL.is_stack_reg src then instr :: k else k | Xparmove(srcs, dsts, itmp, ftmp) -> @@ -408,11 +406,11 @@ let dce_instr instr after k = | ([src], [dst]) -> Xmove(src, dst) :: k | (srcs', dsts') -> Xparmove(srcs', dsts', itmp, ftmp) :: k end - | Xop(op, args, res) -> + | Xop(_, _, res) -> if VSet.mem res after then instr :: k else k - | Xload(chunk, addr, args, dst) -> + | Xload(_, _, _, dst) -> if VSet.mem dst after then instr :: k else k @@ -431,7 +429,7 @@ let rec dce_block blk after = let dead_code_elimination f liveness = { f with fn_code = - PTree.map (fun pc blk -> snd(dce_block blk (PMap.get pc liveness))) + PTree.map (fun pc blk -> Datatypes.snd(dce_block blk (PMap.get pc liveness))) f.fn_code } @@ -454,8 +452,8 @@ let spill_costs f = let charge amount uses v = match v with - | L l -> () - | V(r, ty) -> + | L _ -> () + | V(r, _) -> let st = get_stats r in if st.cost < 0 then (* the variable must be spilled, don't change its cost *) @@ -472,21 +470,21 @@ let spill_costs f = List.iter (charge amount uses) vl in let charge_ros amount ros = - match ros with Coq_inl v -> charge amount 1 v | Coq_inr id -> () in + match ros with Coq_inl v -> charge amount 1 v | Coq_inr _ -> () in let force_stack_allocation v = match v with - | L l -> () - | V(r, ty) -> + | L _ -> () + | V(r,_) -> let st = get_stats r in assert (st.cost < max_int); st.cost <- (-1) in let charge_instr = function | Xmove(src, dst) -> - if is_stack_reg src then + if XTL.is_stack_reg src then force_stack_allocation dst - else if is_stack_reg dst then + else if XTL.is_stack_reg dst then force_stack_allocation src else begin charge 1 1 src; charge 1 1 dst @@ -501,15 +499,15 @@ let spill_costs f = charge_list 1 1 srcs; charge_list 1 1 dsts; charge max_int 0 itmp; charge max_int 0 ftmp (* temps must not be spilled *) - | Xop(op, args, res) -> + | Xop(_, args, res) -> charge_list 10 1 args; charge 10 1 res - | Xload(chunk, addr, args, dst) -> + | Xload(_, _, args, dst) -> charge_list 10 1 args; charge 10 1 dst - | Xstore(chunk, addr, args, src) -> + | Xstore(_, _, args, src) -> charge_list 10 1 args; charge 10 1 src - | Xcall(sg, vos, args, res) -> + | Xcall(_, vos, _, _) -> charge_ros 10 vos - | Xtailcall(sg, vos, args) -> + | Xtailcall(_, vos, _) -> charge_ros 10 vos | Xbuiltin(ef, args, res) -> begin match ef with @@ -528,11 +526,11 @@ let spill_costs f = charge_list 10 1 (params_of_builtin_res res) end | Xbranch _ -> () - | Xcond(cond, args, _, _) -> + | Xcond(_, args, _, _) -> charge_list 10 1 args | Xjumptable(arg, _) -> charge 10 1 arg - | Xreturn optarg -> + | Xreturn _ -> () in let charge_block blk = List.iter charge_instr blk in @@ -595,12 +593,12 @@ let add_interfs_instr g instr live = add_interfs_list g itmp srcs; add_interfs_list g itmp dsts; add_interfs_list g ftmp srcs; add_interfs_list g ftmp dsts; (* Take into account destroyed reg when accessing Incoming param *) - if List.exists (function (L(S(Incoming, _, _))) -> true | _ -> false) srcs + if List.exists (function (L(Locations.S(Incoming, _, _))) -> true | _ -> false) srcs then add_interfs_list g (vmreg temp_for_parent_frame) dsts; (* Take into account destroyed reg when initializing Outgoing arguments of type Tsingle *) if List.exists - (function (L(S(Outgoing, _, Tsingle))) -> true | _ -> false) dsts + (function (L(Locations.S(Outgoing, _, Tsingle))) -> true | _ -> false) dsts then List.iter (fun mr -> @@ -622,17 +620,17 @@ let add_interfs_instr g instr live = (vset_addlist (res :: argl) (VSet.remove res live)) end; add_interfs_destroyed g (VSet.remove res live) (destroyed_by_op op) - | Xload(chunk, addr, args, dst) -> + | Xload(chunk, addr, _, dst) -> add_interfs_def g dst live; add_interfs_destroyed g (VSet.remove dst live) (destroyed_by_load chunk addr) - | Xstore(chunk, addr, args, src) -> + | Xstore(chunk, addr, _,_) -> add_interfs_destroyed g live (destroyed_by_store chunk addr) - | Xcall(sg, vos, args, res) -> + | Xcall(_, _,_, res) -> add_interfs_destroyed g (vset_removelist res live) destroyed_at_call - | Xtailcall(sg, Coq_inl v, args) -> + | Xtailcall(_, Coq_inl v, _) -> List.iter (fun r -> IRC.add_interf g (vmreg r) v) int_callee_save_regs - | Xtailcall(sg, Coq_inr id, args) -> + | Xtailcall(_, Coq_inr _, _) -> () | Xbuiltin(ef, args, res) -> (* Interferences with live across *) @@ -646,7 +644,7 @@ let add_interfs_instr g instr live = | EF_annot_val _, [BA arg], BR res -> (* like a move *) IRC.add_pref g arg res - | EF_inline_asm(txt, sg, clob), _, _ -> + | EF_inline_asm(_, _, clob), _, _ -> let vargs = params_of_builtin_args args in (* clobbered regs interfere with res and args for GCC compatibility *) List.iter (fun c -> @@ -658,13 +656,13 @@ let add_interfs_instr g instr live = clob | _ -> () end - | Xbranch s -> + | Xbranch _ -> () - | Xcond(cond, args, s1, s2) -> + | Xcond(cond, _, _,_) -> add_interfs_destroyed g live (destroyed_by_cond cond) - | Xjumptable(arg, tbl) -> + | Xjumptable _ -> add_interfs_destroyed g live destroyed_by_jumptable - | Xreturn optarg -> + | Xreturn _ -> () let rec add_interfs_block g blk live = @@ -690,16 +688,16 @@ let find_coloring f liveness = (*********** Determination of variables that need spill code insertion *****) let is_reg alloc v = - match alloc v with R _ -> true | S _ -> false + match alloc v with R _ -> true | Locations.S _ -> false let add_tospill alloc v ts = - match alloc v with R _ -> ts | S _ -> VSet.add v ts + match alloc v with R _ -> ts | Locations.S _ -> VSet.add v ts let addlist_tospill alloc vl ts = List.fold_right (add_tospill alloc) vl ts let addros_tospill alloc ros ts = - match ros with Coq_inl v -> add_tospill alloc v ts | Coq_inr s -> ts + match ros with Coq_inl v -> add_tospill alloc v ts | Coq_inr _ -> ts let tospill_instr alloc instr ts = match instr with @@ -707,43 +705,43 @@ let tospill_instr alloc instr ts = if is_reg alloc src || is_reg alloc dst || alloc src = alloc dst then ts else VSet.add src (VSet.add dst ts) - | Xreload(src, dst) -> + | Xreload(_, dst) -> if not (is_reg alloc dst) then begin printf "Error: %a was spilled\n" PrintXTL.var dst; assert false end; ts - | Xspill(src, dst) -> + | Xspill(src, _) -> if not (is_reg alloc src) then begin printf "Error: %a was spilled\n" PrintXTL.var src; assert false end; ts - | Xparmove(srcs, dsts, itmp, ftmp) -> + | Xparmove(_, _, itmp, ftmp) -> assert (is_reg alloc itmp && is_reg alloc ftmp); ts - | Xop(op, args, res) -> + | Xop(_, args, res) -> addlist_tospill alloc args (add_tospill alloc res ts) - | Xload(chunk, addr, args, dst) -> + | Xload(_, _, args, dst) -> addlist_tospill alloc args (add_tospill alloc dst ts) - | Xstore(chunk, addr, args, src) -> + | Xstore(_, _, args, src) -> addlist_tospill alloc args (add_tospill alloc src ts) - | Xcall(sg, vos, args, res) -> + | Xcall(_, vos, _, _) -> addros_tospill alloc vos ts - | Xtailcall(sg, vos, args) -> + | Xtailcall(_, vos, _) -> addros_tospill alloc vos ts | Xbuiltin((EF_annot _ | EF_debug _), _, _) -> ts - | Xbuiltin(ef, args, res) -> + | Xbuiltin(_, args, res) -> addlist_tospill alloc (params_of_builtin_args args) (addlist_tospill alloc (params_of_builtin_res res) ts) - | Xbranch s -> + | Xbranch _ -> ts - | Xcond(cond, args, s1, s2) -> + | Xcond(_, args, _, _) -> addlist_tospill alloc args ts - | Xjumptable(arg, tbl) -> + | Xjumptable(arg, _) -> add_tospill alloc arg ts - | Xreturn optarg -> + | Xreturn _ -> ts let rec tospill_block alloc blk ts = @@ -769,13 +767,13 @@ let tospill_function f alloc = let rec find_reg_containing v = function | [] -> None - | (var, temp, date) :: eqs -> + | (var, temp, _) :: eqs -> if var = v then Some temp else find_reg_containing v eqs let add v t eqs = (v, t, 0) :: eqs let kill x eqs = - List.filter (fun (v, t, date) -> v <> x && t <> x) eqs + List.filter (fun (v, t, _) -> v <> x && t <> x) eqs let reload_var tospill eqs v = if not (VSet.mem v tospill) then @@ -862,11 +860,11 @@ let spill_instr tospill eqs instr = end else begin ([instr], kill dst eqs) end - | Xreload(src, dst) -> + | Xreload _ -> assert false - | Xspill(src, dst) -> + | Xspill _ -> assert false - | Xparmove(srcs, dsts, itmp, ftmp) -> + | Xparmove(_, dsts, _, _) -> ([instr], List.fold_right kill dsts eqs) | Xop(op, args, res) -> begin match is_two_address op args with @@ -906,22 +904,22 @@ let spill_instr tospill eqs instr = let (src', c2, eqs2) = reload_var tospill eqs1 src in (c1 @ c2 @ [Xstore(chunk, addr, args', src')], eqs2) | Xcall(sg, Coq_inl v, args, res) -> - let (v', c1, eqs1) = reload_var tospill eqs v in + let (v', c1, _) = reload_var tospill eqs v in (c1 @ [Xcall(sg, Coq_inl v', args, res)], []) - | Xcall(sg, Coq_inr id, args, res) -> + | Xcall _ -> ([instr], []) | Xtailcall(sg, Coq_inl v, args) -> - let (v', c1, eqs1) = reload_var tospill eqs v in + let (v', c1, _) = reload_var tospill eqs v in (c1 @ [Xtailcall(sg, Coq_inl v', args)], []) - | Xtailcall(sg, Coq_inr id, args) -> + | Xtailcall _ -> ([instr], []) - | Xbuiltin((EF_annot _ | EF_debug _), args, res) -> + | Xbuiltin((EF_annot _ | EF_debug _), _, _) -> ([instr], eqs) | Xbuiltin(ef, args, res) -> let (args', c1, eqs1) = reload_args tospill eqs args in let (res', c2, eqs2) = save_res tospill eqs1 res in (c1 @ Xbuiltin(ef, args', res') :: c2, eqs2) - | Xbranch s -> + | Xbranch _ -> ([instr], eqs) | Xcond(cond, args, s1, s2) -> let (args', c1, eqs1) = reload_vars tospill eqs args in @@ -929,7 +927,7 @@ let spill_instr tospill eqs instr = | Xjumptable(arg, tbl) -> let (arg', c1, eqs1) = reload_var tospill eqs arg in (c1 @ [Xjumptable(arg', tbl)], eqs1) - | Xreturn optarg -> + | Xreturn _ -> ([instr], []) let rec spill_block tospill pc blk eqs = @@ -963,7 +961,7 @@ let spill_function f tospill round = exception Bad_LTL -let mreg_of alloc v = match alloc v with R mr -> mr | S _ -> raise Bad_LTL +let mreg_of alloc v = match alloc v with R mr -> mr | Locations.S _ -> raise Bad_LTL let mregs_of alloc vl = List.map (mreg_of alloc) vl @@ -973,11 +971,11 @@ let make_move src dst k = match src, dst with | R rsrc, R rdst -> if rsrc = rdst then k else LTL.Lop(Omove, [rsrc], rdst) :: k - | R rsrc, S(sl, ofs, ty) -> + | R rsrc, Locations.S(sl, ofs, ty) -> LTL.Lsetstack(rsrc, sl, ofs, ty) :: k - | S(sl, ofs, ty), R rdst -> + | Locations.S(sl, ofs, ty), R rdst -> LTL.Lgetstack(sl, ofs, ty, rdst) :: k - | S _, S _ -> + | Locations.S _, Locations.S _ -> if src = dst then k else raise Bad_LTL type parmove_status = To_move | Being_moved | Moved @@ -997,11 +995,11 @@ let make_parmove srcs dsts itmp ftmp k = match s, d with | R rs, R rd -> code := LTL.Lop(Omove, [rs], rd) :: !code - | R rs, S(sl, ofs, ty) -> + | R rs, Locations.S(sl, ofs, ty) -> code := LTL.Lsetstack(rs, sl, ofs, ty) :: !code - | S(sl, ofs, ty), R rd -> + | Locations.S(sl, ofs, ty), R rd -> code := LTL.Lgetstack(sl, ofs, ty, rd) :: !code - | S(sls, ofss, tys), S(sld, ofsd, tyd) -> + | Locations.S(sls, ofss, tys), Locations.S(sld, ofsd, tyd) -> let tmp = temp_for tys in (* code will be reversed at the end *) code := LTL.Lsetstack(tmp, sld, ofsd, tyd) :: @@ -1054,9 +1052,9 @@ let transl_instr alloc instr k = LTL.Lload(chunk, addr, mregs_of alloc args, mreg_of alloc dst) :: k | Xstore(chunk, addr, args, src) -> LTL.Lstore(chunk, addr, mregs_of alloc args, mreg_of alloc src) :: k - | Xcall(sg, vos, args, res) -> + | Xcall(sg, vos, _, _) -> LTL.Lcall(sg, mros_of alloc vos) :: k - | Xtailcall(sg, vos, args) -> + | Xtailcall(sg, vos, _) -> LTL.Ltailcall(sg, mros_of alloc vos) :: [] | Xbuiltin(ef, args, res) -> LTL.Lbuiltin(ef, List.map (AST.map_builtin_arg alloc) args, @@ -1067,7 +1065,7 @@ let transl_instr alloc instr k = LTL.Lcond(cond, mregs_of alloc args, s1, s2) :: [] | Xjumptable(arg, tbl) -> LTL.Ljumptable(mreg_of alloc arg, tbl) :: [] - | Xreturn optarg -> + | Xreturn _ -> LTL.Lreturn :: [] let rec transl_block alloc blk = diff --git a/backend/Splitting.ml b/backend/Splitting.ml index 17b8098d..f09da104 100644 --- a/backend/Splitting.ml +++ b/backend/Splitting.ml @@ -13,10 +13,8 @@ (* Live range splitting over RTL *) open Camlcoq -open Datatypes open Coqlib open Maps -open AST open Kildall open Registers open RTL @@ -75,7 +73,7 @@ module LRMap = struct let bot : t = RMap.empty - let lub_opt_range r olr1 olr2 = + let lub_opt_range _ olr1 olr2 = match olr1, olr2 with | Some lr1, Some lr2 -> unify lr1 lr2; olr1 | Some _, None -> olr1 diff --git a/backend/XTL.ml b/backend/XTL.ml index 2ddbc50a..7ff26171 100644 --- a/backend/XTL.ml +++ b/backend/XTL.ml @@ -99,11 +99,11 @@ let twin_reg r = let rec successors_block = function | Xbranch s :: _ -> [s] - | Xtailcall(sg, vos, args) :: _ -> [] - | Xcond(cond, args, s1, s2) :: _ -> [s1; s2] - | Xjumptable(arg, tbl) :: _ -> tbl + | Xtailcall(_,_,_) :: _ -> [] + | Xcond(_,_, s1, s2) :: _ -> [s1; s2] + | Xjumptable(_, tbl) :: _ -> tbl | Xreturn _:: _ -> [] - | instr :: blk -> successors_block blk + | _ :: blk -> successors_block blk | [] -> assert false (**** Type checking for XTL *) @@ -159,25 +159,25 @@ let type_instr = function | Xstore(chunk, addr, args, src) -> set_vars_type args (type_of_addressing addr); set_var_type src (type_of_chunk chunk) - | Xcall(sg, Coq_inl v, args, res) -> + | Xcall(_, Coq_inl v, _, _) -> set_var_type v Tint - | Xcall(sg, Coq_inr id, args, res) -> + | Xcall(_, Coq_inr _, _, _) -> () - | Xtailcall(sg, Coq_inl v, args) -> + | Xtailcall(_, Coq_inl v, _) -> set_var_type v Tint - | Xtailcall(sg, Coq_inr id, args) -> + | Xtailcall(_, Coq_inr _,_) -> () | Xbuiltin(ef, args, res) -> let sg = ef_sig ef in type_builtin_args args sg.sig_args; type_builtin_res res (proj_sig_res sg) - | Xbranch s -> + | Xbranch _ -> () - | Xcond(cond, args, s1, s2) -> + | Xcond(cond, args, _, _) -> set_vars_type args (type_of_condition cond) - | Xjumptable(arg, tbl) -> + | Xjumptable(arg, _) -> set_var_type arg Tint - | Xreturn args -> + | Xreturn _ -> () let type_block blk = diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index e4001e6b..c3e07995 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -22,10 +22,10 @@ open Builtins open Camlcoq open AST open Values -open Ctypes -open Cop -open Csyntax -open Initializers +open !Ctypes +open !Cop +open !Csyntax +open !Initializers open Floats (** ** Extracting information about global variables from their atom *) @@ -76,13 +76,13 @@ let atom_sections a = with Not_found -> [] -let atom_is_small_data a ofs = +let atom_is_small_data a _ = try (Hashtbl.find decl_atom a).a_access = Sections.Access_near with Not_found -> false -let atom_is_rel_data a ofs = +let atom_is_rel_data a _ = try (Hashtbl.find decl_atom a).a_access = Sections.Access_far with Not_found -> @@ -106,7 +106,7 @@ let comp_env : composite_env ref = ref Maps.PTree.empty (** Hooks -- overriden in machine-dependent CPragmas module *) -let process_pragma_hook = ref (fun (s: string) -> false) +let process_pragma_hook = ref (fun (_: string) -> false) (** ** Error handling *) @@ -267,7 +267,7 @@ let stringNum = ref 0 (* number of next global for string literals *) let stringTable : (string, AST.ident) Hashtbl.t = Hashtbl.create 47 let wstringTable : (int64 list, AST.ident) Hashtbl.t = Hashtbl.create 47 -let name_for_string_literal env s = +let name_for_string_literal _ s = try Hashtbl.find stringTable s with Not_found -> @@ -297,7 +297,7 @@ let global_for_string s id = (id, Gvar {gvar_info = typeStringLiteral s; gvar_init = !init; gvar_readonly = true; gvar_volatile = false}) -let name_for_wide_string_literal env s = +let name_for_wide_string_literal _ s = try Hashtbl.find wstringTable s with Not_found -> @@ -357,13 +357,11 @@ let make_builtin_memcpy args = let sz1 = match Initializers.constval !comp_env sz with | Errors.OK(Vint n) -> n - | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be -a constant)"; Integers.Int.zero in + | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be a constant)"; Integers.Int.zero in let al1 = match Initializers.constval !comp_env al with | Errors.OK(Vint n) -> n - | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be -a constant)"; Integers.Int.one in + | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be a constant)"; Integers.Int.one in (* to check: sz1 > 0, al1 divides sz1, al1 = 1|2|4|8 *) (* Issue #28: must decay array types to pointer types *) Ebuiltin(EF_memcpy(sz1, al1), @@ -403,9 +401,9 @@ let make_builtin_va_arg_by_ref helper ty arg = Tpointer(Tvoid, noattr)) in Evalof(Ederef(Ecast(call, ty_ptr), ty), ty) -let make_builtin_va_arg env ty e = +let make_builtin_va_arg _ ty e = match ty with - | Tint _ | Tpointer _ -> + | Ctypes.Tint _ | Tpointer _ -> make_builtin_va_arg_by_val "__compcert_va_int32" ty (Tint(I32, Unsigned, noattr)) e | Tlong _ -> @@ -445,7 +443,7 @@ let convertCallconv va unproto attr = (** Types *) let convertIkind = function - | C.IBool -> (Unsigned, IBool) + | C.IBool -> (Unsigned, Ctypes.IBool) | C.IChar -> ((if (!Machine.config).Machine.char_signed then Signed else Unsigned), I8) | C.ISChar -> (Signed, I8) @@ -474,7 +472,7 @@ let checkFunctionType env tres targs = | None -> () | Some l -> List.iter - (fun (id, ty) -> + (fun (_, ty) -> if Cutil.is_composite_type env ty then unsupported "function parameter of struct or union type (consider adding option -fstruct-passing)") l @@ -483,7 +481,7 @@ let checkFunctionType env tres targs = let rec convertTyp env t = match t with - | C.TVoid a -> Tvoid + | C.TVoid _ -> Tvoid | C.TInt(C.ILongLong, a) -> Tlong(Signed, convertAttr a) | C.TInt(C.IULongLong, a) -> @@ -515,13 +513,13 @@ let rec convertTyp env t = Tstruct(intern_string id.name, convertAttr a) | C.TUnion(id, a) -> Tunion(intern_string id.name, convertAttr a) - | C.TEnum(id, a) -> + | C.TEnum(_, a) -> let (sg, sz) = convertIkind Cutil.enum_ikind in Tint(sz, sg, convertAttr a) and convertParams env = function | [] -> Tnil - | (id, ty) :: rem -> Tcons(convertTyp env ty, convertParams env rem) + | (_, ty) :: rem -> Tcons(convertTyp env ty, convertParams env rem) let rec convertTypArgs env tl el = match tl, el with @@ -529,7 +527,7 @@ let rec convertTypArgs env tl el = | [], e1 :: el -> Tcons(convertTyp env (Cutil.default_argument_conversion env e1.etyp), convertTypArgs env [] el) - | (id, t1) :: tl, e1 :: el -> + | (_, t1) :: tl, _ :: el -> Tcons(convertTyp env t1, convertTypArgs env tl el) let convertField env f = @@ -552,8 +550,8 @@ let convertCompositedef env su id attr members = let rec projFunType env ty = match Cutil.unroll env ty with - | TFun(res, args, vararg, attr) -> Some(res, args, vararg) - | TPtr(ty', attr) -> projFunType env ty' + | TFun(res, args, vararg, _) -> Some(res, args, vararg) + | TPtr(ty', _) -> projFunType env ty' | _ -> None let string_of_type ty = @@ -665,7 +663,7 @@ let rec convertExpr env e = | C.EConst(C.CWStr s) -> let ty = typeWideStringLiteral s in Evalof(Evar(name_for_wide_string_literal env s, ty), ty) - | C.EConst(C.CEnum(id, i)) -> + | C.EConst(C.CEnum(_, i)) -> Ctyping.econst_int (convertInt i) Signed | C.ESizeof ty1 -> Ctyping.esizeof (convertTyp env ty1) @@ -693,25 +691,25 @@ let rec convertExpr env e = | C.EBinop((C.Oadd|C.Osub|C.Omul|C.Odiv|C.Omod|C.Oand|C.Oor|C.Oxor| C.Oshl|C.Oshr|C.Oeq|C.One|C.Olt|C.Ogt|C.Ole|C.Oge) as op, - e1, e2, tyres) -> + e1, e2, _) -> let op' = match op with - | C.Oadd -> Oadd - | C.Osub -> Osub - | C.Omul -> Omul - | C.Odiv -> Odiv - | C.Omod -> Omod - | C.Oand -> Oand - | C.Oor -> Oor - | C.Oxor -> Oxor - | C.Oshl -> Oshl - | C.Oshr -> Oshr - | C.Oeq -> Oeq - | C.One -> One - | C.Olt -> Olt - | C.Ogt -> Ogt - | C.Ole -> Ole - | C.Oge -> Oge + | C.Oadd -> Cop.Oadd + | C.Osub -> Cop.Osub + | C.Omul -> Cop.Omul + | C.Odiv -> Cop.Odiv + | C.Omod -> Cop.Omod + | C.Oand -> Cop.Oand + | C.Oor -> Cop.Oor + | C.Oxor -> Cop.Oxor + | C.Oshl -> Cop.Oshl + | C.Oshr -> Cop.Oshr + | C.Oeq -> Cop.Oeq + | C.One -> Cop.One + | C.Olt -> Cop.Olt + | C.Ogt -> Cop.Ogt + | C.Ole -> Cop.Ole + | C.Oge -> Cop.Oge | _ -> assert false in ewrap (Ctyping.ebinop op' (convertExpr env e1) (convertExpr env e2)) | C.EBinop(C.Oassign, e1, e2, _) -> @@ -725,19 +723,19 @@ let rec convertExpr env e = | C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign| C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign| C.Oshl_assign|C.Oshr_assign) as op, - e1, e2, tyres) -> + e1, e2, _) -> let op' = match op with - | C.Oadd_assign -> Oadd - | C.Osub_assign -> Osub - | C.Omul_assign -> Omul - | C.Odiv_assign -> Odiv - | C.Omod_assign -> Omod - | C.Oand_assign -> Oand - | C.Oor_assign -> Oor - | C.Oxor_assign -> Oxor - | C.Oshl_assign -> Oshl - | C.Oshr_assign -> Oshr + | C.Oadd_assign -> Cop.Oadd + | C.Osub_assign -> Cop.Osub + | C.Omul_assign -> Cop.Omul + | C.Odiv_assign -> Cop.Odiv + | C.Omod_assign -> Cop.Omod + | C.Oand_assign -> Cop.Oand + | C.Oor_assign -> Cop.Oor + | C.Oxor_assign -> Cop.Oxor + | C.Oshl_assign -> Cop.Oshl + | C.Oshr_assign -> Cop.Oshr | _ -> assert false in let e1' = convertLvalue env e1 in let e2' = convertExpr env e2 in @@ -754,7 +752,7 @@ let rec convertExpr env e = (convertExpr env e2) (convertExpr env e3)) | C.ECast(ty1, e1) -> ewrap (Ctyping.ecast (convertTyp env ty1) (convertExpr env e1)) - | C.ECompound(ty1, ie) -> + | C.ECompound _ -> unsupported "compound literals"; ezero | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) -> @@ -809,7 +807,7 @@ let rec convertExpr env e = Econs(va_list_ptr(convertExpr env arg), Enil), convertTyp env e.etyp) - | C.ECall({edesc = C.EVar {name = "__builtin_va_arg"}}, [arg1; arg2]) -> + | C.ECall({edesc = C.EVar {name = "__builtin_va_arg"}}, [arg1; _]) -> make_builtin_va_arg env (convertTyp env e.etyp) (convertExpr env arg1) | C.ECall({edesc = C.EVar {name = "__builtin_va_end"}}, _) -> @@ -945,7 +943,7 @@ let rec contains_case s = | C.Sif(_,s1,s2) -> contains_case s1; contains_case s2 | C.Swhile (_,s1) | C.Sdowhile (s1,_) -> contains_case s1 - | C.Sfor (s1,e,s2,s3) -> contains_case s1; contains_case s2; contains_case s3 + | C.Sfor (s1,_,s2,s3) -> contains_case s1; contains_case s2; contains_case s3 | C.Slabeled(C.Scase _, _) -> unsupported "'case' outside of 'switch'" | C.Slabeled(_,s) -> contains_case s @@ -958,13 +956,13 @@ let rec contains_case s = let swrap = function | Errors.OK s -> s | Errors.Error msg -> - error ("retyping error: " ^ string_of_errmsg msg); Sskip + error ("retyping error: " ^ string_of_errmsg msg); Csyntax.Sskip let rec convertStmt env s = updateLoc s.sloc; match s.sdesc with | C.Sskip -> - Sskip + Csyntax.Sskip | C.Sdo e -> swrap (Ctyping.sdo (convertExpr env e)) | C.Sseq(s1, s2) -> @@ -1020,7 +1018,7 @@ let rec convertStmt env s = unsupported "nested blocks"; Sskip | C.Sdecl _ -> unsupported "inner declarations"; Sskip - | C.Sasm(attrs, txt, outputs, inputs, clobber) -> + | C.Sasm(_, txt, outputs, inputs, clobber) -> if not !Clflags.option_finline_asm then unsupported "inline 'asm' statement (consider adding option -finline-asm)"; Sdo (convertAsm s.sloc env txt outputs inputs clobber) @@ -1080,7 +1078,7 @@ let convertFundef loc env fd = a_access = Sections.Access_default; a_inline = fd.fd_inline && not fd.fd_vararg; (* PR#15 *) a_loc = loc }; - (id', Gfun(Internal + (id', Gfun(Csyntax.Internal {fn_return = ret; fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib; fn_params = params; @@ -1091,7 +1089,7 @@ let convertFundef loc env fd = let re_builtin = Str.regexp "__builtin_" -let convertFundecl env (sto, id, ty, optinit) = +let convertFundecl env (_, id, ty, _) = let (args, res, cconv) = match convertTyp env ty with | Tfunction(args, res, cconv) -> (args, res, cconv) @@ -1106,20 +1104,20 @@ let convertFundecl env (sto, id, ty, optinit) = && List.mem_assoc id.name builtins.functions then EF_builtin(id'', sg) else EF_external(id'', sg) in - (id', Gfun(External(ef, args, res, cconv))) + (id', Gfun(Csyntax.External(ef, args, res, cconv))) (** Initializers *) let rec convertInit env init = match init with | C.Init_single e -> - Init_single (convertExpr env e) + Initializers.Init_single (convertExpr env e) | C.Init_array il -> - Init_array (convertInitList env (List.rev il) Init_nil) + Initializers.Init_array (convertInitList env (List.rev il) Init_nil) | C.Init_struct(_, flds) -> - Init_struct (convertInitList env (List.rev_map snd flds) Init_nil) + Initializers.Init_struct (convertInitList env (List.rev_map snd flds) Init_nil) | C.Init_union(_, fld, i) -> - Init_union (intern_string fld.fld_name, convertInit env i) + Initializers.Init_union (intern_string fld.fld_name, convertInit env i) and convertInitList env il accu = match il with @@ -1179,11 +1177,11 @@ let rec convertGlobdecls env res gl = | g :: gl' -> updateLoc g.gloc; match g.gdesc with - | C.Gdecl((sto, id, ty, optinit) as d) -> + | C.Gdecl((_, id, ty, _) as d) -> (* Functions become external declarations. Other types become variable declarations. *) begin match Cutil.unroll env ty with - | TFun(tres, targs, va, a) -> + | TFun(_, targs, _, _) -> if targs = None then warning ("'" ^ id.name ^ "' is declared without a function prototype"); convertGlobdecls env (convertFundecl env d :: res) gl' @@ -1225,7 +1223,7 @@ let rec translEnv env = function let env' = match g.gdesc with | C.Gcompositedecl(su, id, attr) -> - Env.add_composite env id (Cutil.composite_info_decl env su attr) + Env.add_composite env id (Cutil.composite_info_decl su attr) | C.Gcompositedef(su, id, attr, fld) -> Env.add_composite env id (Cutil.composite_info_def env su attr fld) | C.Gtypedef(id, ty) -> @@ -1253,13 +1251,13 @@ let cleanupGlobals p = if IdentSet.mem fd.fd_name !strong then error ("multiple definitions of " ^ fd.fd_name.name); strong := IdentSet.add fd.fd_name !strong - | C.Gdecl(Storage_extern, id, ty, init) -> + | C.Gdecl(Storage_extern, id, _, _) -> extern := IdentSet.add id !extern - | C.Gdecl(sto, id, ty, Some i) -> + | C.Gdecl(_, id, _, Some _) -> if IdentSet.mem id !strong then error ("multiple definitions of " ^ id.name); strong := IdentSet.add id !strong - | C.Gdecl(sto, id, ty, None) -> + | C.Gdecl(_, id, _, None) -> weak := IdentSet.add id !weak | _ -> () in List.iter classify_def p; @@ -1270,7 +1268,7 @@ let cleanupGlobals p = | g :: gl -> updateLoc g.gloc; match g.gdesc with - | C.Gdecl(sto, id, ty, init) -> + | C.Gdecl(sto, id, _, init) -> let better_def_exists = if sto = Storage_extern then IdentSet.mem id !strong || IdentSet.mem id !weak @@ -1291,7 +1289,7 @@ let cleanupGlobals p = let public_globals gl = List.fold_left - (fun accu (id, g) -> if atom_is_static id then accu else id :: accu) + (fun accu (id, _) -> if atom_is_static id then accu else id :: accu) [] gl (** Convert a [C.program] into a [Csyntax.program] *) diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index ed19e178..bcdedd53 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -17,14 +17,12 @@ open Format open Camlcoq -open Datatypes -open Values open AST open PrintAST -open Ctypes +open !Ctypes open Cop open PrintCsyntax -open Clight +open !Clight (* Naming temporaries *) @@ -34,9 +32,7 @@ let temp_name (id: ident) = "$" ^ Z.to_string (Z.Zpos id) (* Precedences and associativity (H&S section 7.2) *) -type associativity = LtoR | RtoL | NA - -let rec precedence = function +let precedence = function | Evar _ -> (16, NA) | Etempvar _ -> (16, NA) | Ederef _ -> (15, RtoL) @@ -138,11 +134,11 @@ let rec print_stmt p s = (temp_name id) print_expr e1 print_expr_list (true, el) - | Sbuiltin(None, ef, tyargs, el) -> + | Sbuiltin(None, ef, _, el) -> fprintf p "@[<hv 2>builtin %s@,(@[<hov 0>%a@]);@]" (name_of_external ef) print_expr_list (true, el) - | Sbuiltin(Some id, ef, tyargs, el) -> + | Sbuiltin(Some id, ef, _, el) -> fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]);@]" (temp_name id) (name_of_external ef) @@ -227,11 +223,11 @@ and print_stmt_for p s = (temp_name id) print_expr e1 print_expr_list (true, el) - | Sbuiltin(None, ef, tyargs, el) -> + | Sbuiltin(None, ef, _, el) -> fprintf p "@[<hv 2>builtin %s@,(@[<hov 0>%a@]);@]" (name_of_external ef) print_expr_list (true, el) - | Sbuiltin(Some id, ef, tyargs, el) -> + | Sbuiltin(Some id, ef, _, el) -> fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]);@]" (temp_name id) (name_of_external ef) @@ -258,10 +254,10 @@ let print_function p id f = let print_fundef p id fd = match fd with - | External(EF_external(_,_), args, res, cconv) -> + | Clight.External(EF_external(_,_), args, res, cconv) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res, cconv))) - | External(_, _, _, _) -> + | Clight.External(_, _, _, _) -> () | Internal f -> print_function p id f diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index bb6576aa..e3e04c07 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -15,16 +15,13 @@ (** Pretty-printer for Csyntax *) -open Printf open Format open Camlcoq -open Datatypes open Values open AST -open Globalenvs -open Ctypes +open !Ctypes open Cop -open Csyntax +open !Csyntax let name_unop = function | Onotbool -> "!" @@ -102,7 +99,7 @@ let rec name_cdecl id ty = | Tfunction _ | Tarray _ -> sprintf "(*%s%s)" (attributes_space a) id | _ -> sprintf "*%s%s" (attributes_space a) id in name_cdecl id' t - | Tarray(t, n, a) -> + | Tarray(t, n, _) -> name_cdecl (sprintf "%s[%ld]" id (camlint_of_coqint n)) t | Tfunction(args, res, cconv) -> let b = Buffer.create 20 in @@ -173,11 +170,11 @@ let rec precedence = function let print_pointer_hook : (formatter -> Values.block * Integers.Int.int -> unit) ref - = ref (fun p (b, ofs) -> ()) + = ref (fun _ _ -> ()) let print_typed_value p v ty = match v, ty with - | Vint n, Tint(I32, Unsigned, _) -> + | Vint n, Ctypes.Tint(I32, Unsigned, _) -> fprintf p "%luU" (camlint_of_coqint n) | Vint n, _ -> fprintf p "%ld" (camlint_of_coqint n) @@ -236,7 +233,7 @@ let rec expr p (prec, e) = expr (prec1, a1) (name_binop op) expr (prec2, a2) | Ecast(a1, ty) -> fprintf p "(%s) %a" (name_type ty) expr (prec', a1) - | Eassign(res, Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _), _) -> + | Eassign(res, Ebuiltin(EF_inline_asm(txt, _, clob), _, args, _), _) -> extended_asm p txt (Some res) args clob | Eassign(a1, a2, _) -> fprintf p "%a =@ %a" expr (prec1, a1) expr (prec2, a2) @@ -262,16 +259,16 @@ let rec expr p (prec, e) = | Ebuiltin(EF_annot_val(txt, _), _, args, _) -> fprintf p "__builtin_annot_val@[<hov 1>(%S%a)@]" (camlstring_of_coqstring txt) exprlist (false, args) - | Ebuiltin(EF_external(id, sg), _, args, _) -> + | Ebuiltin(EF_external(id, _), _, args, _) -> fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args) - | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) -> + | Ebuiltin(EF_inline_asm(txt, _, clob), _, args, _) -> extended_asm p txt None args clob | Ebuiltin(EF_debug(kind,txt,_),_,args,_) -> fprintf p "__builtin_debug@[<hov 1>(%d,%S%a)@]" (P.to_int kind) (extern_atom txt) exprlist (false,args) | Ebuiltin(_, _, args, _) -> fprintf p "<unknown builtin>@[<hov 1>(%a)@]" exprlist (true, args) - | Eparen(a1, tycast, ty) -> + | Eparen(a1, tycast, _) -> fprintf p "(%s) %a" (name_type tycast) expr (prec', a1) end; if prec' < prec then fprintf p ")@]" else fprintf p "@]" @@ -427,12 +424,12 @@ let print_function p id f = let print_fundef p id fd = match fd with - | External(EF_external(_,_), args, res, cconv) -> + | Csyntax.External(EF_external(_,_), args, res, cconv) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res, cconv))) - | External(_, _, _, _) -> + | Csyntax.External(_, _, _, _) -> () - | Internal f -> + | Csyntax.Internal f -> print_function p id f let string_of_init id = @@ -509,7 +506,7 @@ let print_globdef p (id, gd) = let struct_or_union = function Struct -> "struct" | Union -> "union" -let declare_composite p (Composite(id, su, m, a)) = +let declare_composite p (Composite(id, su, _, _)) = fprintf p "%s %s;@ " (struct_or_union su) (extern_atom id) let define_composite p (Composite(id, su, m, a)) = diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 39481bfb..ad3db667 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -37,18 +37,18 @@ let name_of_chunk = function | Many64 -> "any64" let name_of_external = function - | EF_external(name, sg) -> sprintf "extern %S" (camlstring_of_coqstring name) - | EF_builtin(name, sg) -> sprintf "builtin %S" (camlstring_of_coqstring name) + | EF_external(name, _) -> sprintf "extern %S" (camlstring_of_coqstring name) + | EF_builtin(name, _) -> sprintf "builtin %S" (camlstring_of_coqstring name) | EF_vload chunk -> sprintf "volatile load %s" (name_of_chunk chunk) | EF_vstore chunk -> sprintf "volatile store %s" (name_of_chunk chunk) | EF_malloc -> "malloc" | EF_free -> "free" | EF_memcpy(sz, al) -> sprintf "memcpy size %s align %s " (Z.to_string sz) (Z.to_string al) - | EF_annot(text, targs) -> sprintf "annot %S" (camlstring_of_coqstring text) - | EF_annot_val(text, targ) -> sprintf "annot_val %S" (camlstring_of_coqstring text) - | EF_inline_asm(text, sg, clob) -> sprintf "inline_asm %S" (camlstring_of_coqstring text) - | EF_debug(kind, text, targs) -> + | EF_annot(text, _) -> sprintf "annot %S" (camlstring_of_coqstring text) + | EF_annot_val(text, _) -> sprintf "annot_val %S" (camlstring_of_coqstring text) + | EF_inline_asm(text, _, _) -> sprintf "inline_asm %S" (camlstring_of_coqstring text) + | EF_debug(kind, text, _) -> sprintf "debug%d %S" (P.to_int kind) (extern_atom text) let rec print_builtin_arg px oc = function diff --git a/common/Sections.ml b/common/Sections.ml index ec5b6412..b792581f 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -13,8 +13,6 @@ (* *) (* *********************************************************************) -open Camlcoq - (* Handling of linker sections *) type section_name = diff --git a/common/Switchaux.ml b/common/Switchaux.ml index 0d4901bf..35f58aa7 100644 --- a/common/Switchaux.ml +++ b/common/Switchaux.ml @@ -10,7 +10,6 @@ (* *) (* *********************************************************************) -open Datatypes open Camlcoq open Switch diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index bbc39456..6e325ff2 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -19,7 +19,7 @@ open Printf open Machine -open C +open !C open Cutil open Transform @@ -60,12 +60,6 @@ let unsigned_ikind_for_carrier nbits = if nbits <= 8 * !config.sizeof_longlong then IULongLong else assert false -let fits_unsigned v n = - v >= 0L && v < Int64.shift_left 1L n - -let fits_signed v n = - let p = Int64.shift_left 1L (n-1) in v >= Int64.neg p && v < p - let is_signed_enum_bitfield env sid fld eid n = let info = Env.find_enum env eid in if List.for_all (fun (_, v, _) -> int_representable v n false) info.Env.ei_members @@ -73,7 +67,7 @@ let is_signed_enum_bitfield env sid fld eid n = else if List.for_all (fun (_, v, _) -> int_representable v n true) info.Env.ei_members then true else begin - Cerrors.warning "Warning: not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" eid.name fld sid.name n; + Cerrors.warning "Warning: not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" eid.name fld sid.C.name n; false end @@ -519,7 +513,7 @@ let transf_decl env (sto, id, ty, init_opt) = let transf_stmt env s = Transform.stmt - ~expr:(fun loc env ctx e -> transf_exp env ctx e) + ~expr:(fun _ env ctx e -> transf_exp env ctx e) ~decl:transf_decl env s diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml index 74b535d4..7a706da2 100644 --- a/cparser/Ceval.ml +++ b/cparser/Ceval.ml @@ -80,10 +80,10 @@ let boolean_value v = let constant = function | CInt(v, ik, _) -> I (normalize_int v ik) - | CFloat(v, fk) -> raise Notconst + | CFloat _ -> raise Notconst | CStr s -> S s | CWStr s -> WS s - | CEnum(id, v) -> I v + | CEnum(_, v) -> I v let is_signed env ty = match unroll env ty with @@ -91,7 +91,7 @@ let is_signed env ty = | TEnum(_, _) -> is_signed_ikind enum_ikind | _ -> false -let cast env ty_to ty_from v = +let cast env ty_to v = match unroll env ty_to, v with | TInt(IBool, _), _ -> if boolean_value v then I 1L else I 0L @@ -101,11 +101,11 @@ let cast env ty_to ty_from v = if sizeof_ikind ik >= !config.sizeof_ptr then v else raise Notconst - | TPtr(ty, _), I n -> + | TPtr _, I n -> I (normalize_int n (ptr_t_ikind ())) - | TPtr(ty, _), (S _ | WS _) -> + | TPtr _, (S _ | WS _) -> v - | TEnum(_, _), I n -> + | TEnum _, I n -> I (normalize_int n enum_ikind) | _, _ -> raise Notconst @@ -118,12 +118,12 @@ let unop env op tyres ty v = | Olognot, _, _ -> if boolean_value v then I 0L else I 1L | Onot, _, I n -> I (Int64.lognot n) | _ -> raise Notconst - in cast env ty tyres res + in cast env ty res -let comparison env direction ptraction tyop ty1 v1 ty2 v2 = +let comparison env direction ptraction tyop v1 v2 = (* tyop = type at which the comparison is done *) let b = - match cast env tyop ty1 v1, cast env tyop ty2 v2 with + match cast env tyop v1, cast env tyop v2 with | I n1, I n2 -> if is_signed env tyop then direction (compare n1 n2) 0 @@ -143,25 +143,25 @@ let binop env op tyop tyres ty1 v1 ty2 v2 = match op with | Oadd -> if is_arith_type env ty1 && is_arith_type env ty2 then begin - match cast env tyop ty1 v1, cast env tyop ty2 v2 with + match cast env tyop v1, cast env tyop v2 with | I n1, I n2 -> I (Int64.add n1 n2) | _, _ -> raise Notconst end else raise Notconst | Osub -> if is_arith_type env ty1 && is_arith_type env ty2 then begin - match cast env tyop ty1 v1, cast env tyop ty2 v2 with + match cast env tyop v1, cast env tyop v2 with | I n1, I n2 -> I (Int64.sub n1 n2) | _, _ -> raise Notconst end else raise Notconst | Omul -> - begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with + begin match cast env tyop v1, cast env tyop v2 with | I n1, I n2 -> I (Int64.mul n1 n2) | _, _ -> raise Notconst end | Odiv -> - begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with + begin match cast env tyop v1, cast env tyop v2 with | I n1, I n2 -> if n2 = 0L then raise Notconst else if is_signed env tyop then I (Int64.div n1 n2) @@ -206,17 +206,17 @@ let binop env op tyop tyres ty1 v1 ty2 v2 = | _, _ -> raise Notconst end | Oeq -> - comparison env (=) (Some false) tyop ty1 v1 ty2 v2 + comparison env (=) (Some false) tyop v1 v2 | One -> - comparison env (<>) (Some true) tyop ty1 v1 ty2 v2 + comparison env (<>) (Some true) tyop v1 v2 | Olt -> - comparison env (<) None tyop ty1 v1 ty2 v2 + comparison env (<) None tyop v1 v2 | Ogt -> - comparison env (>) None tyop ty1 v1 ty2 v2 + comparison env (>) None tyop v1 v2 | Ole -> - comparison env (<=) None tyop ty1 v1 ty2 v2 + comparison env (<=) None tyop v1 v2 | Oge -> - comparison env (>=) None tyop ty1 v1 ty2 v2 + comparison env (>=) None tyop v1 v2 | Ocomma -> v2 | Ologand -> @@ -229,7 +229,7 @@ let binop env op tyop tyres ty1 v1 ty2 v2 = else if boolean_value v2 then I 1L else I 0L | _ -> raise Notconst (* force normalization of result, e.g. of double to float *) - in cast env tyres tyres res + in cast env tyres res let rec expr env e = match e.edesc with @@ -253,11 +253,10 @@ let rec expr env e = binop env op ty e.etyp e1.etyp (expr env e1) e2.etyp (expr env e2) | EConditional(e1, e2, e3) -> if boolean_value (expr env e1) - then cast env e.etyp e2.etyp (expr env e2) - else cast env e.etyp e3.etyp (expr env e3) - (* | ECast(TInt (_, _), EConst (CFloat (_, _))) -> TODO *) + then cast env e.etyp (expr env e2) + else cast env e.etyp (expr env e3) | ECast(ty, e1) -> - cast env ty e1.etyp (expr env e1) + cast env ty (expr env e1) | ECompound _ -> raise Notconst | ECall _ -> @@ -265,14 +264,14 @@ let rec expr env e = let integer_expr env e = try - match cast env (TInt(ILongLong, [])) e.etyp (expr env e) with + match cast env (TInt(ILongLong, [])) (expr env e) with | I n -> Some n | _ -> None with Notconst -> None let constant_expr env ty e = try - match unroll env ty, cast env ty e.etyp (expr env e) with + match unroll env ty, cast env ty (expr env e) with | TInt(ik, _), I n -> Some(CInt(n, ik, "")) | TPtr(_, _), I n -> Some(CInt(n, IInt, "")) | TPtr(_, _), S s -> Some(CStr s) diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml index fe674d9b..845232aa 100644 --- a/cparser/Cleanup.ml +++ b/cparser/Cleanup.ml @@ -51,18 +51,18 @@ let rec add_typ = function | _ -> () and add_vars vl = - List.iter (fun (id, ty) -> add_typ ty) vl + List.iter (fun (_, ty) -> add_typ ty) vl let rec add_exp e = add_typ e.etyp; (* perhaps not necessary but play it safe *) match e.edesc with - | EConst (CEnum(id, v)) -> addref id + | EConst (CEnum(id, _)) -> addref id | EConst _ -> () | ESizeof ty -> add_typ ty | EAlignof ty -> add_typ ty | EVar id -> addref id - | EUnop(op, e1) -> add_exp e1 - | EBinop(op, e1, e2, ty) -> add_exp e1; add_exp e2 + | EUnop(_, e1) -> add_exp e1 + | EBinop(_, e1, e2, _) -> add_exp e1; add_exp e2 | EConditional(e1, e2, e3) -> add_exp e1; add_exp e2; add_exp e3 | ECast(ty, e1) -> add_typ ty; add_exp e1 | ECompound(ty, ie) -> add_typ ty; add_init ie @@ -74,11 +74,11 @@ and add_init = function | Init_struct(id, il) -> addref id; List.iter (fun (_, i) -> add_init i) il | Init_union(id, _, i) -> addref id; add_init i -let add_decl (sto, id, ty, init) = +let add_decl (_, _, ty, init) = add_typ ty; match init with None -> () | Some i -> add_init i -let add_asm_operand (lbl, cstr, e) = add_exp e +let add_asm_operand (_, _, e) = add_exp e let rec add_stmt s = match s.sdesc with @@ -95,12 +95,12 @@ let rec add_stmt s = | Slabeled(lbl, s) -> begin match lbl with Scase e -> add_exp e | _ -> () end; add_stmt s - | Sgoto lbl -> () + | Sgoto _ -> () | Sreturn None -> () | Sreturn(Some e) -> add_exp e | Sblock sl -> List.iter add_stmt sl | Sdecl d -> add_decl d - | Sasm(attr, template, outputs, inputs, flags) -> + | Sasm(_, _, outputs, inputs, _) -> List.iter add_asm_operand outputs; List.iter add_asm_operand inputs @@ -114,13 +114,13 @@ let add_field f = add_typ f.fld_typ let add_enum e = List.iter - (fun (id, v, opt_e) -> match opt_e with Some e -> add_exp e | None -> ()) + (fun (_, _, opt_e) -> match opt_e with Some e -> add_exp e | None -> ()) e (* Saturate the set of referenced identifiers, starting with externally visible global declarations *) -let visible_decl (sto, id, ty, init) = +let visible_decl (sto, _, ty, _) = sto = Storage_default && match ty with TFun _ -> false | _ -> true @@ -150,7 +150,7 @@ let rec add_needed_globdecls accu = function | [] -> accu | g :: rem -> match g.gdesc with - | Gdecl((sto, id, ty, init) as decl) -> + | Gdecl((_, id, _, _) as decl) -> if needed id then (add_decl decl; add_needed_globdecls accu rem) else add_needed_globdecls (g :: accu) rem @@ -194,14 +194,14 @@ let rec simpl_globdecls accu = function | g :: rem -> let need = match g.gdesc with - | Gdecl((sto, id, ty, init) as decl) -> visible_decl decl || needed id + | Gdecl((_, id, _, _) as decl) -> visible_decl decl || needed id | Gfundef f -> visible_fundef f || needed f.fd_name | Gcompositedecl(_, id, _) -> needed id - | Gcompositedef(_, id, _, flds) -> needed id - | Gtypedef(id, ty) -> needed id + | Gcompositedef(_, id, _, _) -> needed id + | Gtypedef(id, _) -> needed id | Genumdef(id, _, enu) -> needed id || List.exists (fun (id, _, _) -> needed id) enu - | Gpragma s -> true in + | Gpragma _ -> true in if need then simpl_globdecls (g :: accu) rem else begin remove_unused_debug g.gdesc; simpl_globdecls accu rem end diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index e80a4c8e..61441aeb 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -83,7 +83,7 @@ let const pp = function else fprintf pp "\" \"\\x%02Lx\" \"" c) l; fprintf pp "\"" - | CEnum(id, v) -> + | CEnum(id, _) -> ident pp id let attr_arg pp = function @@ -343,11 +343,11 @@ and init pp = function fprintf pp "@[<hov 1>{"; List.iter (fun i -> fprintf pp "%a,@ " init i) il; fprintf pp "}@]" - | Init_struct(id, il) -> + | Init_struct(_, il) -> fprintf pp "@[<hov 1>{"; - List.iter (fun (fld, i) -> fprintf pp "%a,@ " init i) il; + List.iter (fun (_, i) -> fprintf pp "%a,@ " init i) il; fprintf pp "}@]" - | Init_union(id, fld, i) -> + | Init_union(_, fld, i) -> fprintf pp "@[<hov 2>{.%s =@ %a}@]" fld.fld_name init i let simple_decl pp (id, ty) = @@ -450,7 +450,7 @@ let rec stmt pp s = fprintf pp "return;" | Sreturn (Some e) -> fprintf pp "return %a;" exp (0, e) - | Sblock sl -> + | Sblock _ -> fprintf pp "@[<v 2>{@ %a@;<0 -2>}@]" stmt_block s | Sdecl d -> full_decl pp d @@ -535,7 +535,7 @@ let globdecl pp g = | Genumdef(id, attrs, vals) -> fprintf pp "@[<v 2>enum%a %a {" attributes attrs ident id; List.iter - (fun (name, v, opt_e) -> + (fun (name, _, opt_e) -> fprintf pp "@ %a" ident name; begin match opt_e with | None -> () diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index c15a7adf..19f6d29a 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -15,7 +15,6 @@ (* Operations on C types and abstract syntax *) -open Printf open Cerrors open C open Env @@ -74,7 +73,7 @@ let rec find_custom_attributes (names: string list) (al: attributes) = let rec remove_custom_attributes (names: string list) (al: attributes) = match al with | [] -> [] - | Attr(name, args) :: tl when List.mem name names -> + | Attr(name, _) :: tl when List.mem name names -> remove_custom_attributes names tl | a :: tl -> a :: remove_custom_attributes names tl @@ -138,12 +137,12 @@ let rec unroll env t = let rec attributes_of_type env t = match t with | TVoid a -> a - | TInt(ik, a) -> a - | TFloat(fk, a) -> a - | TPtr(ty, a) -> a - | TArray(ty, sz, a) -> add_attributes a (attributes_of_type env ty) - | TFun(ty, params, vararg, a) -> a - | TNamed(s, a) -> attributes_of_type env (unroll env t) + | TInt(_, a) -> a + | TFloat(_, a) -> a + | TPtr(_, a) -> a + | TArray(ty, _, a) -> add_attributes a (attributes_of_type env ty) + | TFun(_, _,_, a) -> a + | TNamed(_, _) -> attributes_of_type env (unroll env t) | TStruct(s, a) -> let ci = Env.find_struct env s in add_attributes ci.ci_attr a | TUnion(s, a) -> @@ -163,7 +162,7 @@ let rec change_attributes_type env (f: attributes -> attributes) t = | TArray(ty, sz, a) -> TArray(change_attributes_type env f ty, sz, f a) | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, f a) - | TNamed(s, a) -> + | TNamed(_, _) -> let t1 = unroll env t in let t2 = change_attributes_type env f t1 in if t2 = t1 then t else t2 (* avoid useless expansion *) @@ -175,7 +174,7 @@ let remove_attributes_type env attr t = change_attributes_type env (fun a -> remove_attributes a attr) t let erase_attributes_type env t = - change_attributes_type env (fun a -> []) t + change_attributes_type env (fun _ -> []) t (* Remove all attributes from type that are not contained in attr *) let strip_attributes_type t attr = @@ -194,7 +193,7 @@ let strip_attributes_type t attr = (* Remove the last attribute from the toplevel and return the changed type *) let strip_last_attribute typ = - let rec hd_opt l = match l with + let hd_opt l = match l with [] -> None,[] | a::rest -> Some a,rest in match typ with @@ -225,7 +224,7 @@ let alignas_attribute al = let rec alignas_attr accu = function | [] -> accu | AAlignas n :: al -> alignas_attr (max n accu) al - | a :: al -> alignas_attr accu al + | _ :: al -> alignas_attr accu al in alignas_attr 0 al (* Type compatibility *) @@ -261,14 +260,14 @@ let combine_types mode env t1 t2 = | None, _ -> sz2 | _, None -> sz1 | Some n1, Some n2 -> if n1 = n2 then Some n2 else raise Incompat - and comp_conv (id, ty) = + and comp_conv (_, ty) = match unroll env ty with - | TInt(kind, attr) -> + | TInt(kind, _) -> begin match kind with | IBool | IChar | ISChar | IUChar | IShort | IUShort -> raise Incompat | _ -> () end - | TFloat(kind, attr) -> + | TFloat(kind, _) -> begin match kind with | FFloat -> raise Incompat | _ -> () @@ -296,7 +295,7 @@ let combine_types mode env t1 t2 = | Some l1, None -> List.iter comp_conv l1; (params1, vararg1) | Some l1, Some l2 -> if List.length l1 <> List.length l2 then raise Incompat; - let comp_param (id1, ty1) (id2, ty2) = + let comp_param (_, ty1) (id2, ty2) = (id2, comp AttrIgnoreTop ty1 ty2) in (Some(List.map2 comp_param l1 l2), comp_base vararg1 vararg2) in @@ -310,8 +309,8 @@ let combine_types mode env t1 t2 = TUnion(comp_base s1 s2, comp_attr m a1 a2) | TEnum(s1, a1), TEnum(s2, a2) -> TEnum(comp_base s1 s2, comp_attr m a1 a2) - | TEnum(s,a1), TInt(enum_ikind,a2) - | TInt(enum_ikind,a2), TEnum (s,a1) -> + | TEnum(s,a1), TInt(_,a2) + | TInt(_,a2), TEnum (s,a1) -> TEnum(s,comp_attr m a1 a2) | _, _ -> raise Incompat @@ -433,7 +432,7 @@ let alignof_struct_union env members = | None -> None | Some a -> align_rec (max a al) rem end else begin - let (s, a, ml') = pack_bitfields ml in + let (_, a, ml') = pack_bitfields ml in align_rec (max a al) ml' end in align_rec 1 members @@ -472,7 +471,7 @@ let rec sizeof env t = | TInt(ik, _) -> Some(sizeof_ikind ik) | TFloat(fk, _) -> Some(sizeof_fkind fk) | TPtr(_, _) -> Some(!config.sizeof_ptr) - | TArray(ty, None, _) -> None + | TArray(_, None, _) -> None | TArray(ty, Some n, _) as t' -> begin match sizeof env ty with | None -> None @@ -561,7 +560,7 @@ let incomplete_type env t = (* Computing composite_info records *) -let composite_info_decl env su attr = +let composite_info_decl su attr = { ci_kind = su; ci_members = []; ci_alignof = None; ci_sizeof = None; ci_attr = attr } @@ -722,7 +721,7 @@ let pointer_decay env t = let unary_conversion env t = match unroll env t with (* Promotion of small integer types *) - | TInt(kind, attr) -> + | TInt(kind, _) -> begin match kind with | IBool | IChar | ISChar | IUChar | IShort | IUShort -> TInt(IInt, []) @@ -730,13 +729,13 @@ let unary_conversion env t = TInt(kind, []) end (* Enums are like signed ints *) - | TEnum(id, attr) -> TInt(enum_ikind, []) + | TEnum(_, _) -> TInt(enum_ikind, []) (* Arrays and functions decay automatically to pointers *) | TArray(ty, _, _) -> TPtr(ty, []) | TFun _ as ty -> TPtr(ty, []) (* Float types and pointer types lose their attributes *) - | TFloat(kind, attr) -> TFloat(kind, []) - | TPtr(ty, attr) -> TPtr(ty, []) + | TFloat(kind, _) -> TFloat(kind, []) + | TPtr(ty, _) -> TPtr(ty, []) (* Other types should not occur, but in doubt... *) | _ -> t @@ -860,7 +859,7 @@ let type_of_constant = function let rec is_lvalue e = match e.edesc with - | EVar id -> true + | EVar _ -> true | EUnop((Oderef | Oarrow _), _) -> true | EUnop(Odot _, e') -> is_lvalue e' | EBinop(Oindex, _, _, _) -> true @@ -892,7 +891,7 @@ let is_literal_0 e = let is_debug_stmt s = let is_debug_call = function - | (ECall ({edesc = EVar id; _},_)) -> id.name = "__builtin_debug" + | (ECall ({edesc = EVar id; _},_)) -> id.C.name = "__builtin_debug" | _ -> false in match s.sdesc with | Sdo {edesc = e;_} -> @@ -906,8 +905,8 @@ let is_debug_stmt s = Custom attributes can safely be dropped or added. *) let valid_assignment_attr afrom ato = - let (afromstd, afromcustom) = List.partition attr_is_standard afrom - and (atostd, atocustom) = List.partition attr_is_standard ato in + let (afromstd, _) = List.partition attr_is_standard afrom + and (atostd,_) = List.partition attr_is_standard ato in incl_attributes afromstd atostd (* Check that an assignment is allowed *) @@ -1032,11 +1031,11 @@ let rec default_init env ty = match unroll env ty with | TInt _ | TEnum _ -> Init_single (intconst 0L IInt) - | TFloat(fk, _) -> + | TFloat(_, _) -> Init_single floatconst0 - | TPtr(ty, _) -> + | TPtr(_, _) -> Init_single nullconst - | TArray(ty, sz, _) -> + | TArray(_, _, _) -> Init_array [] | TStruct(id, _) -> let rec default_init_fields = function diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index b353cba3..3dcfe4aa 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -102,13 +102,11 @@ val sizeof_ikind: ikind -> int (* Return the size of the given integer kind. *) val sizeof_fkind: fkind -> int (* Return the size of the given float kind. *) -val is_signed_ikind: ikind -> bool - (* Return true if the given integer kind is signed, false if unsigned. *) (* Computing composite_info records *) val composite_info_decl: - Env.t -> struct_or_union -> attributes -> Env.composite_info + struct_or_union -> attributes -> Env.composite_info val composite_info_def: Env.t -> struct_or_union -> attributes -> field list -> Env.composite_info val struct_layout: diff --git a/cparser/Elab.ml b/cparser/Elab.ml index d7a1212a..ceab0aa5 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -19,9 +19,9 @@ open Format open Machine -open Cabs +open !Cabs open Cabshelper -open C +open !C open Cutil open Env @@ -90,7 +90,7 @@ let previous_def fn env arg = let redef fn env arg = match previous_def fn env arg with | None -> false - | Some(id, info) -> Env.in_current_scope env id + | Some(id, _) -> Env.in_current_scope env id (* Forward declarations *) @@ -203,7 +203,7 @@ let elab_int_constant loc s0 = in (v, ty) -let elab_float_constant loc f = +let elab_float_constant f = let ty = match f.suffix_FI with | Some ("l"|"L") -> FLongDouble | Some ("f"|"F") -> FFloat @@ -265,7 +265,7 @@ let elab_constant loc = function let (v, ik) = elab_int_constant loc s in CInt(v, ik, s) | CONST_FLOAT f -> - let (v, fk) = elab_float_constant loc f in + let (v, fk) = elab_float_constant f in CFloat(v, fk) | CONST_CHAR(wide, s) -> CInt(elab_char_constant loc wide s, IInt, "") @@ -289,8 +289,8 @@ let elab_attr_arg loc env a = | VARIABLE s -> begin try match Env.lookup_ident env s with - | (id, II_ident(sto, ty)) -> AIdent s - | (id, II_enum v) -> AInt v + | (_, II_ident _) -> AIdent s + | (_, II_enum v) -> AInt v with Env.Error _ -> AIdent s end @@ -319,7 +319,7 @@ let elab_gcc_attr loc env = function warning loc "cannot parse '%s' attribute, ignored" v; [] end -let is_power_of_two n = n > 0L && Int64.(logand n (pred n)) = 0L +let is_power_of_two n = n > 0L && Int64.logand n (Int64.pred n) = 0L let extract_alignas loc a = match a with @@ -477,7 +477,7 @@ let rec elab_specifier ?(only = false) loc env specifier = (* Now the other type specifiers *) | [Cabs.Tnamed id] -> - let (id', info) = wrap Env.lookup_typedef loc env id in + let (id', _) = wrap Env.lookup_typedef loc env id in simple (TNamed(id', [])) | [Cabs.Tstruct_union(STRUCT, id, optmembers, a)] -> @@ -569,7 +569,7 @@ and elab_parameters env params = let (vars, _) = mmap elab_parameter (Env.new_scope env) params in (* Catch special case f(t) where t is void or a typedef to void *) match vars with - | [ ( {name=""}, t) ] when is_void_type env t -> [] + | [ ( {C.name=""}, t) ] when is_void_type env t -> [] | _ -> vars (* Elaboration of a function parameter *) @@ -578,7 +578,7 @@ and elab_parameter env (PARAM (spec, id, decl, attr, loc)) = let (sto, inl, tydef, bty, env1) = elab_specifier loc env spec in if tydef then error loc "'typedef' used in function parameter"; - let ((ty, _), env2) = elab_type_declarator loc env1 bty false decl in + let ((ty, _), _) = elab_type_declarator loc env1 bty false decl in let ty = add_attributes_type (elab_attributes env attr) ty in if sto <> Storage_default && sto <> Storage_register then error loc @@ -702,7 +702,7 @@ and elab_struct_or_union_info kind loc env members attrs = (* Check for incomplete types *) let rec check_incomplete = function | [] -> () - | [ { fld_typ = TArray(ty_elt, None, _) } ] when kind = Struct -> () + | [ { fld_typ = TArray(_, None, _) } ] when kind = Struct -> () (* C99: ty[] allowed as last field of a struct *) | fld :: rem -> if wrap incomplete_type loc env' fld.fld_typ then @@ -726,7 +726,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = Env.lookup_composite env s, s in match optbinding, optmembers with - | Some(tag', ci), None + | Some(tag', _), None when (not only) || Env.in_current_scope env tag' -> (* Reference to an already declared struct or union. Special case: if this is an "only" declaration (without variable names) @@ -753,7 +753,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = (* declaration of an incomplete struct or union *) if tag = "" then error loc "anonymous, incomplete struct or union"; - let ci = composite_info_decl env kind attrs in + let ci = composite_info_decl kind attrs in (* enter it with a new name *) let (tag', env') = Env.enter_composite env tag ci in (* emit it *) @@ -761,7 +761,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = (tag', env') | _, Some members -> (* definition of a complete struct or union *) - let ci1 = composite_info_decl env kind attrs in + let ci1 = composite_info_decl kind attrs in (* enter it, incomplete, with a new name *) let (tag', env') = Env.enter_composite env tag ci1 in (* emit a declaration so that inner structs and unions can refer to it *) @@ -808,7 +808,7 @@ and elab_enum only loc tag optmembers attrs env = if only then fatal_error loc "forward declaration of 'enum %s' is not allowed in ISO C" tag; - let (tag', info) = wrap Env.lookup_enum loc env tag in (tag', env) + let (tag', _) = wrap Env.lookup_enum loc env tag in (tag', env) | Some members -> if tag <> "" && redef Env.lookup_enum env tag then error loc "redefinition of 'enum %s'" tag; @@ -900,18 +900,16 @@ module I = struct * ident (* union type *) * field (* current member *) - type state = zipinit * init (* current point & init for this point *) - (* The initial state: default initialization, current point at top *) let top env name ty = (Ztop(name, ty), default_init env ty) (* Change the initializer for the current point *) - let set (z, i) i' = (z, i') + let set (z, _) i' = (z, i') (* Put the current point back to the top *) let rec to_top = function - | Ztop(name, ty), i as zi -> zi - | Zarray(z, ty, sz, dfl, before, idx, after), i -> + | Ztop _, _ as zi -> zi + | Zarray(z, _, _,_, before, _, after), i -> to_top (z, Init_array (List.rev_append before (i :: after))) | Zstruct(z, id, before, fld, after), i -> to_top (z, Init_struct(id, List.rev_append before ((fld, i) :: after))) @@ -923,34 +921,34 @@ module I = struct (* The type of the current point *) let typeof = function - | Ztop(name, ty), i -> ty - | Zarray(z, ty, sz, dfl, before, idx, after), i -> ty - | Zstruct(z, id, before, fld, after), i -> fld.fld_typ - | Zunion(z, id, fld), i -> fld.fld_typ + | Ztop(_, ty), _ -> ty + | Zarray(_, ty, _, _, _, _, _), _ -> ty + | Zstruct(_, _, _, fld, _), _ -> fld.fld_typ + | Zunion(_, _, fld), _ -> fld.fld_typ (* The name of the path leading to the current point, for error reporting *) let rec zipname = function - | Ztop(name, ty) -> name - | Zarray(z, ty, sz, dfl, before, idx, after) -> + | Ztop(name, _) -> name + | Zarray(z, _, _, _, _, idx, _) -> sprintf "%s[%Ld]" (zipname z) idx - | Zstruct(z, id, before, fld, after) -> + | Zstruct(z, _, _, fld, _) -> sprintf "%s.%s" (zipname z) fld.fld_name - | Zunion(z, id, fld) -> + | Zunion(z, _, fld) -> sprintf "%s.%s" (zipname z) fld.fld_name - let name (z, i) = zipname z + let name (z, _) = zipname z (* Auxiliary functions to deal with arrays *) let index_below (idx: int64) (sz: int64 option) = match sz with None -> true | Some sz -> idx < sz - let il_head dfl = function [] -> dfl | i1 :: il -> i1 - let il_tail = function [] -> [] | i1 :: il -> il + let il_head dfl = function [] -> dfl | ih :: _ -> ih + let il_tail = function [] -> [] | _ :: il -> il (* Advance the current point to the next point in right-up order. Return None if no next point, i.e. we are at top *) let rec next = function - | Ztop(name, ty), i -> None + | Ztop _, _ -> None | Zarray(z, ty, sz, dfl, before, idx, after), i -> let idx' = Int64.succ idx in if index_below idx' sz @@ -975,11 +973,11 @@ module I = struct Some(Zarray(z, ty, sz, dfl, [], 0L, il_tail il), il_head dfl il) end else None - | TStruct(id, _), Init_struct(id', []) -> + | TStruct _, Init_struct(_, []) -> None - | TStruct(id, _), Init_struct(id', (fld1, i1) :: flds) -> + | TStruct(id, _), Init_struct(_, (fld1, i1) :: flds) -> Some(Zstruct(z, id, [], fld1, flds), i1) - | TUnion(id, _), Init_union(id', fld, i) -> + | TUnion(id, _), Init_union(_, fld, i) -> begin match (Env.find_union env id).ci_members with | [] -> None | fld1 :: _ -> @@ -988,7 +986,7 @@ module I = struct then i else default_init env fld1.fld_typ) end - | (TStruct _ | TUnion _), Init_single a -> + | (TStruct _ | TUnion _), Init_single _ -> (* This is a previous whole-struct initialization that we are going to overwrite. Revert to the default initializer. *) first env (z, default_init env ty) @@ -1021,7 +1019,7 @@ module I = struct let rec member env (z, i as zi) name = let ty = typeof zi in match unroll env ty, i with - | TStruct(id, _), Init_struct(id', flds) -> + | TStruct(id, _), Init_struct(_, flds) -> let rec find before = function | [] -> None | (fld, i as f_i) :: after -> @@ -1030,7 +1028,7 @@ module I = struct else find (f_i :: before) after in find [] flds - | TUnion(id, _), Init_union(id', fld, i) -> + | TUnion(id, _), Init_union(_, fld, i) -> if fld.fld_name = name then Some(Zunion(z, id, fld), i) else begin @@ -1043,7 +1041,7 @@ module I = struct find rem in find (Env.find_union env id).ci_members end - | (TStruct _ | TUnion _), Init_single a -> + | (TStruct _ | TUnion _), Init_single _ -> member env (z, default_init env ty) name | _, _ -> None @@ -1128,7 +1126,7 @@ and elab_item zi item il = | CStr _, _ -> error loc "initialization of an array of non-char elements with a string literal"; elab_list zi il false - | CWStr s, TInt(ik, _) -> + | CWStr s, TInt _ -> if not (I.index_below (Int64.of_int(List.length s - 1)) sz) then warning loc "initializer string for array of wide chars %s is too long" (I.name zi); @@ -1231,7 +1229,7 @@ let elab_expr loc env a = | VARIABLE s -> begin match wrap Env.lookup_ident loc env s with - | (id, II_ident(sto, ty)) -> + | (id, II_ident(_, ty)) -> { edesc = EVar id; etyp = ty } | (id, II_enum v) -> { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []) } @@ -1249,7 +1247,7 @@ let elab_expr loc env a = match (unroll env b1.etyp, unroll env b2.etyp) with | (TPtr(t, _) | TArray(t, _, _)), (TInt _ | TEnum _) -> t | (TInt _ | TEnum _), (TPtr(t, _) | TArray(t, _, _)) -> t - | t1, t2 -> error "incorrect types for array subscripting" in + | _, _ -> error "incorrect types for array subscripting" in { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres } | MEMBEROF(a1, fieldname) -> @@ -1302,7 +1300,7 @@ let elab_expr loc env a = | BUILTIN_VA_ARG (a2, a3) -> let ident = match wrap Env.lookup_ident loc env "__builtin_va_arg" with - | (id, II_ident(sto, ty)) -> { edesc = EVar id; etyp = ty } + | (id, II_ident(_, ty)) -> { edesc = EVar id; etyp = ty } | _ -> assert false in let b2 = elab a2 and b3 = elab (TYPE_SIZEOF a3) in @@ -1331,10 +1329,10 @@ let elab_expr loc env a = (* Extract type information *) let (res, args, vararg) = match unroll env b1.etyp with - | TFun(res, args, vararg, a) -> (res, args, vararg) - | TPtr(ty, a) -> + | TFun(res, args, vararg, _) -> (res, args, vararg) + | TPtr(ty, _) -> begin match unroll env ty with - | TFun(res, args, vararg, a) -> (res, args, vararg) + | TFun(res, args, vararg, _) -> (res, args, vararg) | _ -> error "the function part of a call does not have a function type" end | _ -> error "the function part of a call does not have a function type" @@ -1366,7 +1364,7 @@ let elab_expr loc env a = let (ty, _) = elab_type loc env spec dcl in begin match elab_initializer loc env "<compound literal>" ty ie with | (ty', Some i) -> { edesc = ECompound(ty', i); etyp = ty' } - | (ty', None) -> error "ill-formed compound literal" + | (_, None) -> error "ill-formed compound literal" end (* 6.5.3 Unary expressions *) @@ -1489,8 +1487,8 @@ let elab_expr loc env a = else begin let ty = match unroll env b1.etyp, unroll env b2.etyp with - | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> ty - | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> ty + | (TPtr(ty, _) | TArray(ty, _, _)), (TInt _ | TEnum _) -> ty + | (TInt _ | TEnum _), (TPtr(ty, _) | TArray(ty, _, _)) -> ty | _, _ -> error "type error in binary '+'" in if not (pointer_arithmetic_ok env ty) then err "illegal pointer arithmetic in binary '+'"; @@ -1507,16 +1505,16 @@ let elab_expr loc env a = (tyres, tyres) end else begin match unroll env b1.etyp, unroll env b2.etyp with - | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> + | (TPtr(ty, _) | TArray(ty, _, _)), (TInt _ | TEnum _) -> if not (pointer_arithmetic_ok env ty) then err "illegal pointer arithmetic in binary '-'"; (TPtr(ty, []), TPtr(ty, [])) - | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> + | (TInt _ | TEnum _), (TPtr(ty, _) | TArray(ty, _, _)) -> if not (pointer_arithmetic_ok env ty) then err "illegal pointer arithmetic in binary '-'"; (TPtr(ty, []), TPtr(ty, [])) - | (TPtr(ty1, a1) | TArray(ty1, _, a1)), - (TPtr(ty2, a2) | TArray(ty2, _, a2)) -> + | (TPtr(ty1, _) | TArray(ty1, _, _)), + (TPtr(ty2, _) | TArray(ty2, _, _)) -> if not (compatible_types AttrIgnoreAll env ty1 ty2) then err "mismatch between pointer types in binary '-'"; if not (pointer_arithmetic_ok env ty1) then @@ -1587,9 +1585,9 @@ let elab_expr loc env a = | Some ty -> ty in { edesc = EConditional(b1, b2, b3); etyp = tyres } - | TPtr(ty1, a1), TInt _ when is_literal_0 b3 -> + | TPtr(ty1, _), TInt _ when is_literal_0 b3 -> { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, []) } - | TInt _, TPtr(ty2, a2) when is_literal_0 b2 -> + | TInt _, TPtr(ty2, _) when is_literal_0 b2 -> { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, []) } | ty1, ty2 -> match combine_types AttrIgnoreAll env ty1 ty2 with @@ -1727,7 +1725,7 @@ let elab_expr loc env a = | (TInt _ | TEnum _), TPtr _ -> warning "comparison between integer and pointer"; EBinop(op, b1, b2, TPtr(TVoid [], [])) - | ty1, ty2 -> + | _, _ -> error "illegal comparison between types@ %a@ and %a" Cprint.typ b1.etyp Cprint.typ b2.etyp in { edesc = resdesc; etyp = TInt(IInt, []) } @@ -1797,7 +1795,7 @@ let enter_typedefs loc env sto dl = if init <> NO_INIT then error loc "initializer in typedef"; match previous_def Env.lookup_typedef env s with - | Some (s',ty') -> + | Some (_ ,ty') -> if equal_types env ty ty' then begin warning loc "redefinition of typedef '%s'" s; env @@ -1848,7 +1846,7 @@ let enter_or_refine_ident local loc env s sto ty = | Storage_register,_ -> Storage_register in (id, new_sto, Env.add_ident env id new_sto new_ty,new_ty) - | Some(id, II_enum v) when Env.in_current_scope env id -> + | Some(id, II_enum _) when Env.in_current_scope env id -> error loc "redefinition of enumerator '%s'" s; (id, sto, Env.add_ident env id sto ty,ty) | _ -> @@ -1860,7 +1858,7 @@ let enter_decdefs local loc env sto dl = fatal_error loc "'register' on global declaration"; if sto <> Storage_default && dl = [] then warning loc "Storage class specifier on empty declaration"; - let rec enter_decdef (decls, env) (s, ty, init) = + let enter_decdef (decls, env) (s, ty, init) = let isfun = is_function_type env ty in if sto = Storage_extern && init <> NO_INIT then error loc "'extern' declaration cannot have an initializer"; @@ -1915,7 +1913,7 @@ let elab_fundef env spec name defs body loc = fatal_error loc "Parameter '%s' appears more than once in function declaration" id) params; (* Check that the declarations only declare parameters *) - let extract_name (Init_name(Name(s, dty, attrs, loc') as name, ie)) = + let extract_name (Init_name(Name(s, _, _, loc') as name, ie)) = if not (List.mem s params) then error loc' "Declaration of '%s' which is not a function parameter" s; if ie <> NO_INIT then @@ -1936,7 +1934,7 @@ let elab_fundef env spec name defs body loc = "Illegal declaration of function parameter" in let (kr_params_defs, env1) = mmap elab_kr_param_def env1 defs in let kr_params_defs = List.concat kr_params_defs in - let rec search_param_type param = + let search_param_type param = match List.filter (fun (p, _) -> p = param) kr_params_defs with | [] -> (* Parameter is not declared, defaults to "int" in ISO C90, @@ -1949,7 +1947,7 @@ let elab_fundef env spec name defs body loc = in let params' = List.map search_param_type params in (TFun(ty_ret, Some params', false, attr), env1) - | _, Some params -> assert false + | _, Some _ -> assert false in (* Extract info from type *) let (ty_ret, params, vararg, attr) = @@ -1960,7 +1958,7 @@ let elab_fundef env spec name defs body loc = (ty_ret, params, vararg, attr) | _ -> fatal_error loc "wrong type for function definition" in (* Enter function in the environment, for recursive references *) - let (fun_id, sto1, env1,ty) = enter_or_refine_ident false loc env1 s sto ty in + let (fun_id, sto1, env1, _) = enter_or_refine_ident false loc env1 s sto ty in (* Enter parameters in the environment *) let env2 = List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty) @@ -2095,7 +2093,7 @@ let rec elab_stmt env ctx s = begin match Ceval.integer_expr env a' with | None -> error loc "argument of 'case' must be an integer compile-time constant" - | Some n -> () + | Some _ -> () end; { sdesc = Slabeled(Scase a', elab_stmt env ctx s1); sloc = elab_loc loc } diff --git a/cparser/Env.ml b/cparser/Env.ml index 65df6cb9..9ab5e657 100644 --- a/cparser/Env.ml +++ b/cparser/Env.ml @@ -118,15 +118,9 @@ let lookup_ident env s = with Not_found -> raise(Error(Unbound_identifier s)) -let lookup_tag env s = - try - IdentMap.lookup s env.env_tag - with Not_found -> - raise(Error(Unbound_tag(s, "tag"))) - let lookup_struct env s = try - let (id, ci as res) = IdentMap.lookup s env.env_tag in + let (_, ci as res) = IdentMap.lookup s env.env_tag in if ci.ci_kind <> Struct then raise(Error(Tag_mismatch(s, "struct", "union"))); res @@ -135,7 +129,7 @@ let lookup_struct env s = let lookup_union env s = try - let (id, ci as res) = IdentMap.lookup s env.env_tag in + let (_, ci as res) = IdentMap.lookup s env.env_tag in if ci.ci_kind <> Union then raise(Error(Tag_mismatch(s, "union", "struct"))); res @@ -169,11 +163,6 @@ let find_ident env id = with Not_found -> raise(Error(Unbound_identifier(id.name))) -let find_tag env id = - try IdentMap.find id env.env_tag - with Not_found -> - raise(Error(Unbound_tag(id.name, "tag"))) - let find_struct env id = try let ci = IdentMap.find id env.env_tag in @@ -256,7 +245,7 @@ let add_typedef env id info = { env with env_typedef = IdentMap.add id info env.env_typedef } let add_enum env id info = - let add_enum_item env (id, v, exp) = + let add_enum_item env (id, v, _) = { env with env_ident = IdentMap.add id (II_enum v) env.env_ident } in List.fold_left add_enum_item { env with env_enum = IdentMap.add id info env.env_enum } diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml index 94fcda31..5183df9b 100644 --- a/cparser/ExtendedAsm.ml +++ b/cparser/ExtendedAsm.ml @@ -33,7 +33,6 @@ open Printf open Machine open C open Cutil -open Env open Cerrors (* Renaming of labeled and numbered operands *) @@ -151,7 +150,7 @@ let transf_outputs loc env = function when substituting the text *) let rec bind_outputs pos subst = function | [] -> (None, [], subst, pos, pos) - | (lbl, cstr, e) :: outputs -> + | (lbl, _, _) :: outputs -> bind_outputs (pos + 1) (set_label_reg lbl pos pos subst) outputs in bind_outputs 0 StringMap.empty outputs diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index bcf2ada0..b2b00e8c 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -17,8 +17,7 @@ open Lexing open Pre_parser open Pre_parser_aux -open Cabshelper -open Camlcoq +open !Cabshelper module SSet = Set.Make(String) @@ -430,7 +429,7 @@ and singleline_comment = parse open Streams open Specif open Parser - open Aut.GramDefs + open !Aut.GramDefs (* This is the main entry point to the lexer. *) @@ -578,7 +577,7 @@ and singleline_comment = parse let rec doConcat wide str = try match Queue.peek tokens with - | STRING_LITERAL (wide', str', loc) -> + | STRING_LITERAL (wide', str', _) -> ignore (Queue.pop tokens); let (wide'', str'') = doConcat wide' str' in if str'' <> [] diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index 6ea5d121..6a60dfb8 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -127,10 +127,10 @@ let transf_composite loc env su id attrs ml = (* Accessor functions *) -let lookup_function loc env name = +let lookup_function env name = match Env.lookup_ident env name with - | (id, II_ident(sto, ty)) -> (id, ty) - | (id, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name)) + | (id, II_ident(_, ty)) -> (id, ty) + | (_, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name)) (* Type for the access *) @@ -161,14 +161,14 @@ let bswap_read loc env lval = try if !use_reversed then begin let (id, fty) = - lookup_function loc env (sprintf "__builtin_read%d_reversed" bsize) in + lookup_function env (sprintf "__builtin_read%d_reversed" bsize) in let fn = {edesc = EVar id; etyp = fty} in let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lval)] in let call = {edesc = ECall(fn, args); etyp = aty} in ecast_opt env ty call end else begin let (id, fty) = - lookup_function loc env (sprintf "__builtin_bswap%d" bsize) in + lookup_function env (sprintf "__builtin_bswap%d" bsize) in let fn = {edesc = EVar id; etyp = fty} in let args = [ecast_opt env aty lval] in let call = {edesc = ECall(fn, args); etyp = aty} in @@ -188,14 +188,14 @@ let bswap_write loc env lhs rhs = try if !use_reversed then begin let (id, fty) = - lookup_function loc env (sprintf "__builtin_write%d_reversed" bsize) in + lookup_function env (sprintf "__builtin_write%d_reversed" bsize) in let fn = {edesc = EVar id; etyp = fty} in let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lhs); ecast_opt env aty rhs] in {edesc = ECall(fn, args); etyp = TVoid[]} end else begin let (id, fty) = - lookup_function loc env (sprintf "__builtin_bswap%d" bsize) in + lookup_function env (sprintf "__builtin_bswap%d" bsize) in let fn = {edesc = EVar id; etyp = fty} in let args = [ecast_opt env aty rhs] in let call = {edesc = ECall(fn, args); etyp = aty} in @@ -387,7 +387,7 @@ let rec transf_globdecls env accu = function | [] -> List.rev accu | g :: gl -> match g.gdesc with - | Gdecl((sto, id, ty, init) as d) -> + | Gdecl((sto, id, ty, _) as d) -> transf_globdecls (Env.add_ident env id sto ty) ({g with gdesc = Gdecl(transf_decl g.gloc env d)} :: accu) @@ -403,7 +403,7 @@ let rec transf_globdecls env accu = function | Union -> attr | Struct -> remove_custom_attributes ["packed";"__packed__"] attr in transf_globdecls - (Env.add_composite env id (composite_info_decl env su attr')) + (Env.add_composite env id (composite_info_decl su attr')) ({g with gdesc = Gcompositedecl(su, id, attr')} :: accu) gl | Gcompositedef(su, id, attr, fl) -> @@ -422,7 +422,7 @@ let rec transf_globdecls env accu = function (Env.add_enum env id {ei_members = el; ei_attr = attr}) (g :: accu) gl - | Gpragma p -> + | Gpragma _ -> transf_globdecls env (g :: accu) gl (* Program *) diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 664f6a28..0d92c514 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -182,7 +182,7 @@ and stmt_desc env = function | Sgoto lbl -> Sgoto lbl | Sreturn a -> Sreturn (optexp env a) | Sblock sl -> let (sl', _) = mmap stmt_or_decl env sl in Sblock sl' - | Sdecl d -> assert false + | Sdecl _ -> assert false | Sasm(attr, txt, outputs, inputs, flags) -> Sasm(attr, txt, List.map (asm_operand env) outputs, diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml index 4e019380..95f133bd 100644 --- a/cparser/StructReturn.ml +++ b/cparser/StructReturn.ml @@ -19,7 +19,7 @@ open Machine open Configuration -open C +open !C open Cutil open Transform @@ -217,7 +217,7 @@ let rec transf_type env t = TFun(tres', None, vararg, attr) | Ret_ref -> TFun(TVoid [], None, vararg, add_attributes attr attr_structret) - | Ret_value(ty, sz, al) -> + | Ret_value(ty, _, _) -> TFun(ty, None, vararg, attr) end | TFun(tres, Some args, vararg, attr) -> @@ -230,7 +230,7 @@ let rec transf_type env t = let res = Env.fresh_ident "_res" in TFun(TVoid [], Some((res, TPtr(tres', [])) :: args'), vararg, add_attributes attr attr_structret) - | Ret_value(ty, sz, al) -> + | Ret_value(ty, _, _) -> TFun(ty, Some args', vararg, attr) end | TPtr(t1, attr) -> @@ -251,7 +251,7 @@ and transf_funargs env = function (id, t') :: args' | Param_ref_caller -> (id, TPtr(t', [])) :: args' - | Param_flattened(n, sz, al) -> + | Param_flattened(n, _, _) -> list_map_n (fun _ -> (Env.fresh_ident id.name, uint)) n @ args' @@ -261,7 +261,7 @@ let rec translates_to_extended_lvalue arg = is_lvalue arg || (match arg.edesc with | ECall _ -> true - | EBinop(Ocomma, a, b, _) -> translates_to_extended_lvalue b + | EBinop(Ocomma, _, b, _) -> translates_to_extended_lvalue b | _ -> false) let rec transf_expr env ctx e = @@ -279,7 +279,7 @@ let rec transf_expr env ctx e = {edesc = EUnop(op, transf_expr env Val e1); etyp = newty} | EBinop(Oassign, lhs, {edesc = ECall(fn, args); etyp = ty}, _) -> transf_call env ctx (Some (transf_expr env Val lhs)) fn args ty - | EBinop(Ocomma, e1, e2, ty) -> + | EBinop(Ocomma, e1, e2, _) -> ecomma (transf_expr env Effects e1) (transf_expr env ctx e2) | EBinop(op, e1, e2, ty) -> {edesc = EBinop(op, transf_expr env Val e1, @@ -349,7 +349,7 @@ and transf_call env ctx opt_lhs fn args ty = ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []} (eassign lhs tmp) end - | Ret_value(ty_ret, sz, al) -> + | Ret_value(ty_ret, _, _) -> let ecall = {edesc = ECall(fn', args'); etyp = ty_ret} in begin match ctx, opt_lhs with | Effects, None -> @@ -461,7 +461,7 @@ let rec transf_stmt s = {s with sdesc = Sswitch(transf_expr Val e, transf_stmt s1)} | Slabeled(lbl, s1) -> {s with sdesc = Slabeled(lbl, transf_stmt s1)} - | Sgoto lbl -> s + | Sgoto _ -> s | Sreturn None -> s | Sreturn(Some e) -> let e' = transf_expr Val e in @@ -524,7 +524,7 @@ let rec transf_funparams loc env params = ((x, tpx) :: params', actions, IdentMap.add x estarx subst) - | Param_flattened(n, sz, al) -> + | Param_flattened(n, _, _) -> let y = new_temp ~name:x.name (ty_buffer n) in let yparts = list_map_n (fun _ -> Env.fresh_ident x.name) n in let assign_part e p act = @@ -559,7 +559,7 @@ let transf_fundef env f = TVoid [], (vres, tres) :: params, transf_funbody env (subst_stmt subst f.fd_body) (Some eeres)) - | Ret_value(ty, sz, al) -> + | Ret_value(ty, _, _) -> (f.fd_attrib, ty, params, @@ -573,7 +573,7 @@ let transf_fundef env f = (* Composites *) -let transf_composite env su id attr fl = +let transf_composite env _ _ attr fl = (attr, List.map (fun f -> {f with fld_typ = transf_type env f.fld_typ}) fl) (* Entry point *) @@ -591,5 +591,5 @@ let program p = ~decl:transf_decl ~fundef:transf_fundef ~composite:transf_composite - ~typedef:(fun env id ty -> transf_type env ty) + ~typedef:(fun env _ ty -> transf_type env ty) p diff --git a/cparser/Transform.ml b/cparser/Transform.ml index 840234b8..685ef7e1 100644 --- a/cparser/Transform.ml +++ b/cparser/Transform.ml @@ -45,7 +45,7 @@ let new_temp ?(name = "t") ty = let attributes_to_remove_from_temp = add_attributes [AConst] [AVolatile] -let mk_temp env ?(name = "t") ty = +let mk_temp env ty = new_temp (remove_attributes_type env attributes_to_remove_from_temp ty) (* Bind a l-value to a temporary variable if it is not invariant. *) @@ -141,7 +141,7 @@ let expand_postincrdecr ~read ~write env ctx op l = and preserving the statement structure. If [decl] is not given, it applies only to unblocked code. *) -let stmt ~expr ?(decl = fun env decl -> assert false) env s = +let stmt ~expr ?(decl = fun _ _ -> assert false) env s = let rec stm s = match s.sdesc with | Sskip -> s @@ -163,7 +163,7 @@ let stmt ~expr ?(decl = fun env decl -> assert false) env s = {s with sdesc = Sswitch(expr s.sloc env Val e, stm s1)} | Slabeled(lbl, s) -> {s with sdesc = Slabeled(lbl, stm s)} - | Sgoto lbl -> s + | Sgoto _ -> s | Sreturn None -> s | Sreturn (Some e) -> {s with sdesc = Sreturn(Some(expr s.sloc env Val e))} @@ -191,12 +191,12 @@ let fundef trstmt env f = (* Generic transformation of a program *) let program - ?(decl = fun env d -> d) - ?(fundef = fun env fd -> fd) - ?(composite = fun env su id attr fl -> (attr, fl)) - ?(typedef = fun env id ty -> ty) - ?(enum = fun env id attr members -> (attr, members)) - ?(pragma = fun env s -> s) + ?(decl = fun _ d -> d) + ?(fundef = fun _ fd -> fd) + ?(composite = fun _ _ _ attr fl -> (attr, fl)) + ?(typedef = fun _ _ ty -> ty) + ?(enum = fun _ _ attr members -> (attr, members)) + ?(pragma = fun _ s -> s) p = let rec transf_globdecls env accu = function @@ -204,14 +204,14 @@ let program | g :: gl -> let (desc', env') = match g.gdesc with - | Gdecl((sto, id, ty, init) as d) -> + | Gdecl((sto, id, ty, _) as d) -> (Gdecl(decl env d), Env.add_ident env id sto ty) | Gfundef f -> (Gfundef(fundef env f), Env.add_ident env f.fd_name f.fd_storage (fundef_typ f)) | Gcompositedecl(su, id, attr) -> (Gcompositedecl(su, id, attr), - Env.add_composite env id (composite_info_decl env su attr)) + Env.add_composite env id (composite_info_decl su attr)) | Gcompositedef(su, id, attr, fl) -> let (attr', fl') = composite env su id attr fl in (Gcompositedef(su, id, attr', fl'), diff --git a/cparser/Transform.mli b/cparser/Transform.mli index a04896a9..dbd8e575 100644 --- a/cparser/Transform.mli +++ b/cparser/Transform.mli @@ -18,7 +18,7 @@ val reset_temps : unit -> unit val get_temps : unit -> C.decl list val new_temp_var : ?name:string -> C.typ -> C.ident val new_temp : ?name:string -> C.typ -> C.exp -val mk_temp : Env.t -> ?name:string -> C.typ -> C.exp +val mk_temp : Env.t -> C.typ -> C.exp (** Avoiding repeated evaluation of a l-value *) diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index ef8bc91c..eaf49164 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -46,13 +46,13 @@ let rec local_initializer env path init k = (array_init (Int64.succ pos) il') end in array_init 0L il - | Init_struct(id, fil) -> + | Init_struct(_, fil) -> let field_init (fld, i) k = local_initializer env { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ } i k in List.fold_right field_init fil k - | Init_union(id, fld, i) -> + | Init_union(_, fld, i) -> local_initializer env { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ } i k @@ -64,17 +64,6 @@ let add_inits_stmt loc inits s = (fun e s -> sseq loc {sdesc = Sdo e; sloc = loc} s) inits s -(* Prepend assignments to the given expression. *) -(* Associate to the left so that it prints more nicely *) - -let add_inits_expr inits e = - match inits with - | [] -> e - | i1 :: il -> - let comma a b = - { edesc = EBinop(Ocomma, a, b, b.etyp); etyp = b.etyp } in - comma (List.fold_left comma i1 il) e - (* Record new variables to be locally or globally defined *) let local_variables = ref ([]: decl list) @@ -304,7 +293,7 @@ let rec unblock_stmt env ctx ploc s = | Slabeled(lbl, s1) -> add_lineno ctx ploc s.sloc {s with sdesc = Slabeled(lbl, unblock_stmt env ctx s.sloc s1)} - | Sgoto lbl -> + | Sgoto _ -> add_lineno ctx ploc s.sloc s | Sreturn None -> add_lineno ctx ploc s.sloc s @@ -322,7 +311,7 @@ let rec unblock_stmt env ctx ploc s = id:: ctx else ctx in unblock_block env ctx' ploc sl - | Sdecl d -> + | Sdecl _ -> assert false | Sasm(attr, template, outputs, inputs, clob) -> let expand_asm_operand (lbl, cstr, e) = @@ -357,7 +346,7 @@ let unblock_fundef env f = (* Simplification of compound literals within a top-level declaration *) -let unblock_decl loc env ((sto, id, ty, optinit) as d) = +let unblock_decl env ((sto, id, ty, optinit) as d) = match optinit with | None -> [d] | Some init -> @@ -375,8 +364,8 @@ let rec unblock_glob env accu = function | [] -> List.rev accu | g :: gl -> match g.gdesc with - | Gdecl((sto, id, ty, init) as d) -> - let dl = unblock_decl g.gloc env d in + | Gdecl d -> + let dl = unblock_decl env d in unblock_glob env (List.rev_append (List.map (fun d' -> {g with gdesc = Gdecl d'}) dl) @@ -387,7 +376,7 @@ let rec unblock_glob env accu = function unblock_glob env ({g with gdesc = Gfundef f'} :: accu) gl | Gcompositedecl(su, id, attr) -> unblock_glob - (Env.add_composite env id (composite_info_decl env su attr)) + (Env.add_composite env id (composite_info_decl su attr)) (g :: accu) gl | Gcompositedef(su, id, attr, fl) -> unblock_glob diff --git a/debug/Debug.ml b/debug/Debug.ml index 775a0903..7403d7c2 100644 --- a/debug/Debug.ml +++ b/debug/Debug.ml @@ -12,9 +12,8 @@ open AST open BinNums -open C +open !C open Camlcoq -open Dwarfgen open DwarfTypes open Sections @@ -32,7 +31,7 @@ type implem = add_fun_addr: atom -> section_name -> (int * int) -> unit; generate_debug_info: (atom -> string) -> string -> debug_entries option; all_files_iter: (string -> unit) -> unit; - insert_local_declaration: storage -> ident -> typ -> location -> unit; + insert_local_declaration: storage -> ident -> C.typ -> location -> unit; atom_local_variable: ident -> atom -> unit; enter_scope: int -> int -> int -> unit; enter_function_scope: int -> int -> unit; diff --git a/debug/Debug.mli b/debug/Debug.mli index 387491c2..f044b1ad 100644 --- a/debug/Debug.mli +++ b/debug/Debug.mli @@ -11,7 +11,7 @@ (* *********************************************************************) open AST -open C +open !C open Camlcoq open DwarfTypes open BinNums diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index 105b6aad..e8f1703a 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -51,7 +51,7 @@ let types: (int,debug_types) Hashtbl.t = Hashtbl.create 7 let lookup_types: (string, int) Hashtbl.t = Hashtbl.create 7 (* Translate a C.typ to a string needed for hashing *) -let typ_to_string (ty: typ) = +let typ_to_string ty = let buf = Buffer.create 7 in let chan = Format.formatter_of_buffer buf in Cprint.print_debug_idents := true; @@ -64,13 +64,13 @@ let typ_to_string (ty: typ) = let strip_attributes typ = strip_attributes_type typ [AConst; AVolatile] (* Find the type id to an type *) -let find_type (ty: typ) = +let find_type ty = (* We are only interested in Const and Volatile *) let ty = strip_attributes ty in Hashtbl.find lookup_types (typ_to_string ty) (* Add type and information *) -let insert_type (ty: typ) = +let insert_type ty = let insert d_ty ty = let id = next_id () and name = typ_to_string ty in @@ -104,7 +104,7 @@ let insert_type (ty: typ) = arr_size= s; } in ArrayType arr - | TFun (t,param,va,_) -> + | TFun (t,param,_,_) -> let param,prot = (match param with | None -> [],false | Some p -> List.map (fun (i,t) -> let t = attr_aux t in diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml index 17a90536..24712b27 100644 --- a/debug/DebugInit.ml +++ b/debug/DebugInit.ml @@ -10,12 +10,6 @@ (* *) (* *********************************************************************) -open AST -open BinNums -open C -open Camlcoq -open Dwarfgen -open DwarfTypes open Debug let default_debug = diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index ef44a2d5..9313b6c5 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -33,9 +33,6 @@ module DwarfPrinter(Target: DWARF_TARGET): let string_of_comment s = sprintf " %s %s" comment s - let add_comment buf s = - Buffer.add_string buf (sprintf " %s %s" comment s) - (* Byte value to string *) let string_of_byte value ct = sprintf " .byte %s%s\n" (if value then "0x1" else "0x0") (string_of_comment ct) @@ -67,8 +64,6 @@ module DwarfPrinter(Target: DWARF_TARGET): let add_member_size = add_abbr_entry (0x0b,"DW_AT_byte_size",DW_FORM_udata) - let add_high_pc = add_abbr_entry (0x12,"DW_AT_high_pc",DW_FORM_addr) - let add_low_pc = add_abbr_entry (0x11,"DW_AT_low_pc",DW_FORM_addr) let add_declaration = add_abbr_entry (0x3c,"DW_AT_declaration",DW_FORM_flag) @@ -115,7 +110,7 @@ module DwarfPrinter(Target: DWARF_TARGET): if has_sibling then add_abbr_entry (0x1,"DW_AT_sibling",DW_FORM_ref4) buf; in (match entity.tag with - | DW_TAG_array_type e -> + | DW_TAG_array_type _ -> prologue 0x1 "DW_TAG_array_type"; add_type buf | DW_TAG_base_type b -> @@ -623,9 +618,9 @@ module DwarfPrinter(Target: DWARF_TARGET): let name = if e.section_name <> ".text" then Some e.section_name else None in section oc (Section_debug_info name); print_debug_info oc e.start_label e.line_label e.entry) entries; - if List.exists (fun e -> match e.locs with _,[] -> false | _,_ -> true) entries then begin + if List.exists (fun e -> match e.dlocs with _,[] -> false | _,_ -> true) entries then begin section oc Section_debug_loc; - List.iter (fun e -> print_location_list oc e.locs) entries + List.iter (fun e -> print_location_list oc e.dlocs) entries end let print_ranges oc r = diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli index 2af64c0b..f6074cf3 100644 --- a/debug/DwarfTypes.mli +++ b/debug/DwarfTypes.mli @@ -12,7 +12,6 @@ (* Types used for writing dwarf debug information *) -open BinNums open Camlcoq open Sections @@ -285,7 +284,7 @@ type diab_entry = start_label: int; line_label: int; entry: dw_entry; - locs: dw_locations; + dlocs: dw_locations; } type diab_entries = diab_entry list diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index d070e3a9..fe0764e8 100644 --- a/debug/Dwarfgen.ml +++ b/debug/Dwarfgen.ml @@ -534,7 +534,7 @@ let diab_gen_compilation_section s defs acc = start_label = debug_start; line_label = line_start; entry = cp; - locs = Some low_pc,accu.locs; + dlocs = Some low_pc,accu.locs; }::acc let gen_diab_debug_info sec_name var_section : debug_entries = diff --git a/driver/Configuration.mli b/driver/Configuration.mli index 1d048ac4..abfd3ab4 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -12,27 +12,37 @@ val arch: string (** Target architecture *) + val model: string (** Sub-model for this architecture *) + val abi: string (** ABI to use *) + val system: string (** Flavor of operating system that runs CompCert *) val prepro: string list (** How to invoke the external preprocessor *) + val asm: string list (** How to invoke the external assembler *) + val linker: string list (** How to invoke the external linker *) + val asm_supports_cfi: bool (** True if the assembler supports Call Frame Information *) + val stdlib_path: string (** Path to CompCert's library *) + val has_runtime_lib: bool (** True if CompCert's library is available. *) + val has_standard_headers: bool (** True if CompCert's standard header files is available. *) + val advanced_debug: bool (** True if advanced debug is implement for the Target *) @@ -52,6 +62,7 @@ type struct_return_style = val struct_passing_style: struct_passing_style (** Calling conventions to use for passing structs and unions as first-class values *) + val struct_return_style: struct_return_style (** Calling conventions to use for returning structs and unions as first-class values *) diff --git a/driver/Driver.ml b/driver/Driver.ml index bbd949e0..7b245e6e 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -58,7 +58,7 @@ let command ?stdout args = if stdout <> None then Unix.close fd_out; match status with | Unix.WEXITED rc -> rc - | Unix.WSIGNALED n | Unix.WSTOPPED n -> + | Unix.WSIGNALED _ | Unix.WSTOPPED _ -> eprintf "Command '%s' killed on a signal.\n" argv.(0); -1 with Unix.Unix_error(err, fn, param) -> eprintf "Error executing '%s': %s: %s %s\n" @@ -159,7 +159,7 @@ let parse_c_file sourcename ifile = PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax; close_out oc end; - csyntax,None + csyntax (* Dump Asm code in asm format for the validator *) @@ -174,7 +174,7 @@ let dump_jasm asm sourcename destfile = (* From CompCert C AST to asm *) -let compile_c_ast sourcename csyntax ofile debug = +let compile_c_ast sourcename csyntax ofile = (* Prepare to dump Clight, RTL, etc, if requested *) let set_dest dst opt ext = dst := if !opt then Some (output_filename sourcename ".c" ext) @@ -200,14 +200,14 @@ let compile_c_ast sourcename csyntax ofile debug = dump_jasm asm sourcename (output_filename sourcename ".c" !sdump_suffix); (* Print Asm in text form *) let oc = open_out ofile in - PrintAsm.print_program oc asm debug; + PrintAsm.print_program oc asm; close_out oc (* From C source to asm *) let compile_c_file sourcename ifile ofile = - let ast,debug = parse_c_file sourcename ifile in - compile_c_ast sourcename ast ofile debug + let ast = parse_c_file sourcename ifile in + compile_c_ast sourcename ast ofile (* From Cminor to asm *) @@ -232,7 +232,7 @@ let compile_cminor_file ifile ofile = exit 2 | Errors.OK p -> let oc = open_out ofile in - PrintAsm.print_program oc p None; + PrintAsm.print_program oc p; close_out oc with Parsing.Parse_error -> eprintf "File %s, character %d: Syntax error\n" @@ -304,7 +304,7 @@ let process_c_file sourcename = let name = if !option_interp then begin Machine.config := Machine.compcert_interpreter !Machine.config; - let csyntax,_ = parse_c_file sourcename preproname in + let csyntax = parse_c_file sourcename preproname in if not !option_dprepro then safe_remove preproname; Interp.execute csyntax; @@ -338,7 +338,7 @@ let process_c_file sourcename = let process_i_file sourcename = ensure_inputfile_exists sourcename; if !option_interp then begin - let csyntax,_ = parse_c_file sourcename sourcename in + let csyntax = parse_c_file sourcename sourcename in Interp.execute csyntax; "" end else if !option_S then begin @@ -438,7 +438,7 @@ let perform_actions () = let explode_comma_option s = match Str.split (Str.regexp ",") s with | [] -> assert false - | hd :: tl -> tl + | _ :: tl -> tl let version_string = if Version.buildnr <> "" && Version.tag <> "" then @@ -681,13 +681,13 @@ let cmdline_actions = Exact "-fall", Self (fun _ -> set_all language_support_options); Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) - Exact "-g", Self (fun s -> option_g := true; + Exact "-g", Self (fun _ -> option_g := true; option_gdwarf := 3); - Exact "-gdwarf-2", Self (fun s -> option_g:=true; + Exact "-gdwarf-2", Self (fun _ -> option_g:=true; option_gdwarf := 2); - Exact "-gdwarf-3", Self (fun s -> option_g := true; + Exact "-gdwarf-3", Self (fun _ -> option_g := true; option_gdwarf := 3); - Exact "-frename-static", Self (fun s -> option_rename_static:= true); + Exact "-frename-static", Self (fun _ -> option_rename_static:= true); Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin option_g := false end else begin diff --git a/driver/Interp.ml b/driver/Interp.ml index fb1c85f0..8dd4a7c9 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -12,20 +12,17 @@ (* Interpreting CompCert C sources *) -open Format +open !Format open Camlcoq -open Datatypes open AST open Integers open Values open Memory open Globalenvs open Events -open Ctypes -open Cop -open Csyntax +open !Ctypes +open !Csyntax open Csem -open Clflags (* Configuration *) @@ -84,18 +81,18 @@ let name_of_fundef prog fd = | [] -> "<unknown function>" | (id, Gfun fd') :: rem -> if fd == fd' then extern_atom id else find_name rem - | (id, Gvar v) :: rem -> + | (_, Gvar _) :: rem -> find_name rem - in find_name prog.prog_defs + in find_name prog.Csyntax.prog_defs let name_of_function prog fn = let rec find_name = function | [] -> "<unknown function>" - | (id, Gfun(Internal fn')) :: rem -> + | (id, Gfun(Csyntax.Internal fn')) :: rem -> if fn == fn' then extern_atom id else find_name rem - | (id, _) :: rem -> + | _ :: rem -> find_name rem - in find_name prog.prog_defs + in find_name prog.Csyntax.prog_defs let invert_local_variable e b = Maps.PTree.fold @@ -121,22 +118,22 @@ let print_val_list p vl = let print_state p (prog, ge, s) = match s with - | State(f, s, k, e, m) -> + | State(f, s, _, e, _) -> PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e; fprintf p "in function %s, statement@ @[<hv 0>%a@]" (name_of_function prog f) PrintCsyntax.print_stmt s - | ExprState(f, r, k, e, m) -> + | ExprState(f, r, _, e, _) -> PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e; fprintf p "in function %s, expression@ @[<hv 0>%a@]" (name_of_function prog f) PrintCsyntax.print_expr r - | Callstate(fd, args, k, m) -> + | Callstate(fd, args, _, _) -> PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv Maps.PTree.empty; fprintf p "calling@ @[<hov 2>%s(%a)@]" (name_of_fundef prog fd) print_val_list args - | Returnstate(res, k, m) -> + | Returnstate(res, _, _) -> PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv Maps.PTree.empty; fprintf p "returning@ %a" print_val res @@ -223,10 +220,10 @@ let rank_state = function | Stuckstate -> assert false let mem_state = function - | State(f, s, k, e, m) -> m - | ExprState(f, r, k, e, m) -> m - | Callstate(fd, args, k, m) -> m - | Returnstate(res, k, m) -> m + | State(_, _, _, _, m) -> m + | ExprState(_, _, _, _, m) -> m + | Callstate(_, _, _, m) -> m + | Returnstate(_, _, m) -> m | Stuckstate -> assert false let compare_state s1 s2 = @@ -397,14 +394,14 @@ let do_external_function id sg ge w args m = | _ -> None -let do_inline_assembly txt sg ge w args m = None +let do_inline_assembly _ _ _ _ _ _ = None (* Implementing external functions producing observable events *) let rec world ge m = lazy (Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m)) -and world_io ge m id args = +and world_io _ _ _ _ = None and world_vload ge m chunk id ofs = @@ -419,7 +416,7 @@ and world_vstore ge m chunk id ofs ev = Mem.store chunk m b ofs v >>= fun m' -> Some(world ge m') -let do_event p ge time w ev = +let do_event p _ time w ev = if !trace >= 1 then fprintf p "@[<hov 2>Time %d: observable event:@ %a@]@." time print_event ev; @@ -441,30 +438,30 @@ let rec do_events p ge time w t = let (|||) a b = a || b (* strict boolean or *) -let diagnose_stuck_expr p ge w f a kont e m = +let diagnose_stuck_expr p ge w _ a _ e m = let rec diagnose k a = (* diagnose subexpressions first *) let found = match k, a with - | LV, Ederef(r, ty) -> diagnose RV r - | LV, Efield(r, f, ty) -> diagnose RV r - | RV, Evalof(l, ty) -> diagnose LV l - | RV, Eaddrof(l, ty) -> diagnose LV l - | RV, Eunop(op, r1, ty) -> diagnose RV r1 - | RV, Ebinop(op, r1, r2, ty) -> diagnose RV r1 ||| diagnose RV r2 - | RV, Ecast(r1, ty) -> diagnose RV r1 - | RV, Econdition(r1, r2, r3, ty) -> diagnose RV r1 - | RV, Eassign(l1, r2, ty) -> diagnose LV l1 ||| diagnose RV r2 - | RV, Eassignop(op, l1, r2, tyres, ty) -> diagnose LV l1 ||| diagnose RV r2 - | RV, Epostincr(id, l, ty) -> diagnose LV l - | RV, Ecomma(r1, r2, ty) -> diagnose RV r1 - | RV, Eparen(r1, tycast, ty) -> diagnose RV r1 - | RV, Ecall(r1, rargs, ty) -> diagnose RV r1 ||| diagnose_list rargs - | RV, Ebuiltin(ef, tyargs, rargs, ty) -> diagnose_list rargs + | LV, Ederef(r, _) -> diagnose RV r + | LV, Efield(r, _, _) -> diagnose RV r + | RV, Evalof(l, _) -> diagnose LV l + | RV, Eaddrof(l, _) -> diagnose LV l + | RV, Eunop(_, r1, _) -> diagnose RV r1 + | RV, Ebinop(_, r1, r2, _) -> diagnose RV r1 ||| diagnose RV r2 + | RV, Ecast(r1, _) -> diagnose RV r1 + | RV, Econdition(r1, _, _, _) -> diagnose RV r1 + | RV, Eassign(l1, r2, _) -> diagnose LV l1 ||| diagnose RV r2 + | RV, Eassignop(_, l1, r2, _, _) -> diagnose LV l1 ||| diagnose RV r2 + | RV, Epostincr(_, l, _) -> diagnose LV l + | RV, Ecomma(r1, _, _) -> diagnose RV r1 + | RV, Eparen(r1, _, _) -> diagnose RV r1 + | RV, Ecall(r1, rargs, _) -> diagnose RV r1 ||| diagnose_list rargs + | RV, Ebuiltin(_, _, rargs, _) -> diagnose_list rargs | _, _ -> false in if found then true else begin let l = Cexec.step_expr ge do_external_function do_inline_assembly e w k a m in - if List.exists (fun (ctx,red) -> red = Cexec.Stuckred) l then begin + if List.exists (fun (_,red) -> red = Cexec.Stuckred) l then begin PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e; fprintf p "@[<hov 2>Stuck subexpression:@ %a@]@." PrintCsyntax.print_expr a; @@ -499,7 +496,7 @@ let do_step p prog ge time s w = | None -> let l = Cexec.do_step ge do_external_function do_inline_assembly w s in if l = [] - || List.exists (fun (Cexec.TR(r,t,s)) -> s = Stuckstate) l + || List.exists (fun (Cexec.TR(_,_,s)) -> s = Stuckstate) l then begin pp_set_max_boxes p 1000; fprintf p "@[<hov 2>Stuck state: %a@]@." print_state (prog, ge, s); @@ -532,7 +529,7 @@ let rec explore_one p prog ge time s w = let rec explore_all p prog ge time states = if !trace >= 2 then begin List.iter - (fun (n, s, w) -> + (fun (n, s, _) -> fprintf p "@[<hov 2>State %d.%d: @ %a@]@." time n print_state (prog, ge, s)) states @@ -582,9 +579,9 @@ let world_program prog = else {gv with gvar_init = []} in (id, Gvar gv') - | Gfun fd -> + | Gfun _ -> (id, gd) in - {prog with prog_defs = List.map change_def prog.prog_defs} + {prog with Csyntax.prog_defs = List.map change_def prog.Csyntax.prog_defs} (* Massaging the program to get a suitable "main" function *) @@ -599,7 +596,7 @@ let change_main_function p old_main old_main_ty = fn_params = []; fn_vars = []; fn_body = body } in let new_main_id = intern_string "___main" in { prog_main = new_main_id; - prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs; + Csyntax.prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.Csyntax.prog_defs; prog_public = p.prog_public; prog_types = p.prog_types; prog_comp_env = p.prog_comp_env } @@ -607,10 +604,10 @@ let change_main_function p old_main old_main_ty = let rec find_main_function name = function | [] -> None | (id, Gfun fd) :: gdl -> if id = name then Some fd else find_main_function name gdl - | (id, Gvar v) :: gdl -> find_main_function name gdl + | (_, Gvar _) :: gdl -> find_main_function name gdl let fixup_main p = - match find_main_function p.prog_main p.prog_defs with + match find_main_function p.Csyntax.prog_main p.prog_defs with | None -> fprintf err_formatter "ERROR: no main() function@."; None diff --git a/lib/Printlines.mli b/lib/Printlines.mli index 79201f86..545eb033 100644 --- a/lib/Printlines.mli +++ b/lib/Printlines.mli @@ -20,8 +20,10 @@ type filebuf val openfile: string -> filebuf (** Open the file with the given name. *) + val close: filebuf -> unit (** Close the file underlying the given buffer. *) + val copy: out_channel -> string -> filebuf -> int -> int -> unit (** [copy oc pref buf first last] copies lines number [first] to [last], included, to the channel [oc]. Each line is 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 |