diff options
Diffstat (limited to 'tools')
-rw-r--r-- | tools/modorder.ml | 112 | ||||
-rw-r--r-- | tools/ndfun.ml | 23 |
2 files changed, 130 insertions, 5 deletions
diff --git a/tools/modorder.ml b/tools/modorder.ml new file mode 100644 index 00000000..34e157d0 --- /dev/null +++ b/tools/modorder.ml @@ -0,0 +1,112 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Parse dependencies generated by ocamldep and produce a linking order *) + +open Printf + +type status = Todo | Inprogress | Done + +type node = { + deps: string list; + result: string; + mutable status: status +} + +(* Parsing *) + +let re_continuation_line = Str.regexp "\\(.*\\)\\\\[ \t]*$" + +let re_depend_line = Str.regexp "\\([^ ]+\\) *:\\(.*\\)$" + +let re_whitespace = Str.regexp "[ \t\n]+" + +let parse_dependencies depfile = + let deps = (Hashtbl.create 63 : (string, node) Hashtbl.t) in + let ic = open_in depfile in + + let rec read_line () = + let l = input_line ic in + if Str.string_match re_continuation_line l 0 then begin + let l' = Str.matched_group 1 l in + l' ^ read_line () + end else + l in + + let enter_line l = + if not (Str.string_match re_depend_line l 0) then begin + eprintf "Warning: ill-formed dependency line '%s'\n" l + end else begin + let lhs = Str.matched_group 1 l + and rhs = Str.matched_group 2 l in + let node = { + deps = Str.split re_whitespace rhs; + result = rhs; + status = Todo + } in + Hashtbl.add deps lhs node + end in + + begin try + while true do enter_line (read_line ()) done + with End_of_file -> + () + end; + close_in ic; + deps + +(* Suffix of a file name *) + +let re_suffix = Str.regexp "\\.[a-zA-Z]+$" + +let filename_suffix s = + try + ignore (Str.search_forward re_suffix s 0); Str.matched_string s + with Not_found -> + "" + +(* Topological sorting *) + +let emit_dependencies deps targets = + + let rec dsort target suff = + match (try Some(Hashtbl.find deps target) with Not_found -> None) with + | None -> () + | Some node -> + match node.status with + | Done -> () + | Inprogress -> + eprintf "Warning: cyclic dependency on '%s', ignored\n" target + | Todo -> + node.status <- Inprogress; + List.iter + (fun dep -> + if Filename.check_suffix dep suff then dsort dep suff) + node.deps; + printf "%s " target; + node.status <- Done + in + Array.iter (fun t -> dsort t (filename_suffix t)) targets + +let _ = + if Array.length Sys.argv < 3 then begin + eprintf "Usage: modorder <dependency file> <target>...\n"; + exit 2 + end; + emit_dependencies + (parse_dependencies Sys.argv.(1)) + (Array.sub Sys.argv 2 (Array.length Sys.argv - 2)); + print_newline() + diff --git a/tools/ndfun.ml b/tools/ndfun.ml index 78fb03d5..4ee07e54 100644 --- a/tools/ndfun.ml +++ b/tools/ndfun.ml @@ -1,3 +1,20 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Preprocessor for .vp files *) + open Printf (* Error reporting *) @@ -9,11 +26,7 @@ let error file line msg = (* Replace newlines with spaces *) let oneline s = - let t = String.create (String.length s) in - for i = 0 to String.length s - 1 do - t.[i] <- (match s.[i] with '\n' -> ' ' | c -> c) - done; - t + String.map (function '\n' -> ' ' | c -> c) s (* Trim leading and terminating spaces, and compress multiple spaces *) |