From c130f4936bad11fd6dab3a5d142b870d2a5f650c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 29 Dec 2014 11:15:29 +0100 Subject: Use Unix.create_process instead of Sys.command (continued). --- driver/Configuration.ml | 125 ++++++++++++++++++++++++------------------------ driver/Driver.ml | 88 +++++++++++++++++++++------------- 2 files changed, 119 insertions(+), 94 deletions(-) (limited to 'driver') diff --git a/driver/Configuration.ml b/driver/Configuration.ml index e73125f7..0012dc0c 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -10,86 +10,87 @@ (* *) (* *********************************************************************) +open Printf -let config_vars: (string, string) Hashtbl.t = Hashtbl.create 10 +(* Locate the .ini file, which is either in the same directory as + the executable or in the directory ../share *) +let ini_file_name = + try + Sys.getenv "COMPCERT_CONFIG" + with Not_found -> + let exe_dir = Filename.dirname Sys.executable_name in + let exe_ini = Filename.concat exe_dir "compcert.ini" in + let share_dir = + Filename.concat (Filename.concat exe_dir Filename.parent_dir_name) + "share" in + let share_ini = Filename.concat share_dir "compcert.ini" in + if Sys.file_exists exe_ini then exe_ini + else if Sys.file_exists share_ini then share_ini + else begin + eprintf "Cannot find compcert.ini configuration file.\n"; + exit 2 + end + +(* Read in the .ini file *) -(* Read in the .ini file, which is either in the same directory or in the directory ../share *) let _ = try - let file = - try - let env_file = Sys.getenv "COMPCERT_CONFIG" in - open_in env_file - with Not_found -> - let dir = Sys.getcwd () - and name = Sys.executable_name in - let dirname = if Filename.is_relative name then - Filename.dirname (Filename.concat dir name) - else - Filename.dirname name - in - let share_dir = Filename.concat (Filename.concat dirname Filename.parent_dir_name) "share" in - try - open_in (Filename.concat dirname "compcert.ini") - with Sys_error _ -> - open_in (Filename.concat share_dir "compcert.ini") - in - (try - let ini_line = Str.regexp "\\([^=]+\\)=\\(.+\\)" in - while true do - let line = input_line file in - if Str.string_match ini_line line 0 then - let key = Str.matched_group 1 line - and value = Str.matched_group 2 line in - Hashtbl.add config_vars key value - else - Printf.eprintf "Wrong value %s in .ini file.\n" line - done - with End_of_file -> close_in file) - with Sys_error msg -> Printf.eprintf "Unable to open .ini file\n" + Readconfig.read_config_file ini_file_name + with + | Readconfig.Error(file, lineno, msg) -> + eprintf "Error reading configuration file %s.\n" ini_file_name; + eprintf "%s:%d:%s\n" file lineno msg; + exit 2 + | Sys_error msg -> + eprintf "Error reading configuration file %s.\n" ini_file_name; + eprintf "%s\n" msg; + exit 2 let get_config key = - try - Hashtbl.find config_vars key - with Not_found -> - Printf.eprintf "Configuration option `%s' is not set\n" key; exit 2 + match Readconfig.key_val key with + | Some v -> v + | None -> eprintf "Configuration option `%s' is not set\n" key; exit 2 -let bad_config key v = - Printf.eprintf "Invalid value `%s' for configuation option `%s'\n" v key; exit 2 +let bad_config key vl = + eprintf "Invalid value `%s' for configuration option `%s'\n" + (String.concat " " vl) key; + exit 2 -let prepro = get_config "prepro" -let asm = get_config "asm" -let linker = get_config "linker" -let arch = - let v = get_config "arch" in - (match v with - | "powerpc" - | "arm" - | "ia32" -> () - | _ -> bad_config "arch" v); - v +let get_config_string key = + match get_config key with + | [v] -> v + | vl -> bad_config key vl -let model = get_config "model" -let abi = get_config "abi" -let system = get_config "system" +let get_config_list key = + match get_config key with + | [] -> bad_config key [] + | vl -> vl + +let prepro = get_config_list "prepro" +let asm = get_config_list "asm" +let linker = get_config_list "linker" +let arch = + match get_config_string "arch" with + | "powerpc"|"arm"|"ia32" as a -> a + | v -> bad_config "arch" [v] +let model = get_config_string "model" +let abi = get_config_string "abi" +let system = get_config_string "system" let has_runtime_lib = - match get_config "has_runtime_lib" with + match get_config_string "has_runtime_lib" with | "true" -> true | "false" -> false - | v -> bad_config "has_runtime_lib" v - - + | v -> bad_config "has_runtime_lib" [v] let stdlib_path = if has_runtime_lib then - get_config "stdlib_path" + get_config_string "stdlib_path" else "" - let asm_supports_cfi = - match get_config "asm_supports_cfi" with + match get_config_string "asm_supports_cfi" with | "true" -> true | "false" -> false - | v -> bad_config "asm_supports_cfi" v + | v -> bad_config "asm_supports_cfi" [v] -let version = get_config "version" +let version = get_config_string "version" diff --git a/driver/Driver.ml b/driver/Driver.ml index fec87420..14ce11f4 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -20,17 +20,38 @@ open Timing let stdlib_path = ref Configuration.stdlib_path -let command cmd = +(* Invocation of external tools *) + +let command ?stdout args = if !option_v then begin - prerr_string "+ "; prerr_string cmd; prerr_endline "" + eprintf "+ %s" (String.concat " " args); + begin match stdout with + | None -> () + | Some f -> eprintf " > %s" f + end; + prerr_endline "" end; - Sys.command cmd - -let quote_options opts = - String.concat " " (List.rev_map Filename.quote opts) - -let quote_arguments args = - String.concat " " (List.map Filename.quote args) + let argv = Array.of_list args in + assert (Array.length argv > 0); + try + let fd_out = + match stdout with + | None -> Unix.stdout + | Some f -> + Unix.openfile f [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o666 in + let pid = + Unix.create_process argv.(0) argv Unix.stdin fd_out Unix.stderr in + let (_, status) = + Unix.waitpid [] pid in + if stdout <> None then Unix.close fd_out; + match status with + | Unix.WEXITED rc -> rc + | Unix.WSIGNALED n | Unix.WSTOPPED n -> + 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" + argv.(0) fn (Unix.error_message err) param; + -1 let safe_remove file = try Sys.remove file with Sys_error _ -> () @@ -68,16 +89,17 @@ let output_filename_default default_file = let preprocess ifile ofile = let output = - if ofile = "-" then "" else sprintf "> %s" ofile in - let cmd = - sprintf "%s -D__COMPCERT__ %s %s %s %s" - Configuration.prepro - (if Configuration.has_runtime_lib - then sprintf "-I%s" !stdlib_path - else "") - (quote_options !prepro_options) - ifile output in - if command cmd <> 0 then begin + if ofile = "-" then None else Some ofile in + let cmd = List.concat [ + Configuration.prepro; + ["-D__COMPCERT__"]; + (if Configuration.has_runtime_lib + then ["-I" ^ !stdlib_path] + else []); + List.rev !prepro_options; + [ifile] + ] in + if command ?stdout:output cmd <> 0 then begin if ofile <> "-" then safe_remove ofile; eprintf "Error during preprocessing.\n"; exit 2 @@ -208,11 +230,13 @@ let compile_cminor_file ifile ofile = (* From asm to object file *) let assemble ifile ofile = - let cmd = - sprintf "%s -o %s %s %s" - Configuration.asm ofile (quote_options !assembler_options) ifile in - let retcode = command cmd in - if retcode <> 0 then begin + let cmd = List.concat [ + Configuration.asm; + ["-o"; ofile]; + List.rev !assembler_options; + [ifile] + ] in + if command cmd <> 0 then begin safe_remove ofile; eprintf "Error during assembling.\n"; exit 2 @@ -221,14 +245,14 @@ let assemble ifile ofile = (* Linking *) let linker exe_name files = - let cmd = - sprintf "%s -o %s %s %s" - Configuration.linker - (Filename.quote exe_name) - (quote_arguments files) - (if Configuration.has_runtime_lib - then sprintf "-L%s -lcompcert" !stdlib_path - else "") in + let cmd = List.concat [ + Configuration.linker; + ["-o"; exe_name]; + files; + (if Configuration.has_runtime_lib + then ["-L" ^ !stdlib_path; "-lcompcert"] + else []) + ] in if command cmd <> 0 then exit 2 (* Processing of a .c file *) -- cgit From f2b1c25aa56a27836652aef3feeee0856c04235c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 8 Feb 2015 16:41:45 +0100 Subject: Interpreter produces more detailed trace, including name of semantic rules used. Cexec: record names of rules used in every reduction. Interp: print these rule names in -trace mode. Also: simplified the exploration in "-all" mode; give unique names to states. Csem: fix name of reduction rule "red_call". --- driver/Interp.ml | 156 ++++++++++++++++++++++--------------------------------- 1 file changed, 61 insertions(+), 95 deletions(-) (limited to 'driver') diff --git a/driver/Interp.ml b/driver/Interp.ml index ab22cebb..2725dbfe 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -254,28 +254,14 @@ let compare_state s1 s2 = compare (rank_state s1) (rank_state s2) end -(* Sets of states already explored *) +(* Maps of states already explored. *) -module StateSet = - Set.Make(struct - type t = state * Determinism.world - let compare (s1,w1) (s2,w2) = compare_state s1 s2 +module StateMap = + Map.Make(struct + type t = state + let compare = compare_state end) -(* Purging states that will never be reached again based on their memory - next block. All states with nextblock <= the given nextblock are - removed. We take advantage of the fact that StateSets are sorted - by increasing nextblock, cf. the definition of compare_state above. *) - -let rec purge_seen nextblock seen = - let min = try Some(StateSet.min_elt seen) with Not_found -> None in - match min with - | None -> seen - | Some((s, w) as sw) -> - if P.le (mem_state s).Mem.nextblock nextblock - then purge_seen nextblock (StateSet.remove sw seen) - else seen - (* Extract a string from a global pointer *) let extract_string m blk ofs = @@ -435,7 +421,7 @@ and world_vstore ge m chunk id ofs ev = let do_event p ge time w ev = if !trace >= 1 then - fprintf p "@[Time %d: observable event:@ @[%a@]@]@." + fprintf p "@[Time %d: observable event:@ %a@]@." time print_event ev; (* Return new world after external action *) match ev with @@ -497,11 +483,10 @@ let diagnose_stuck_state p ge w = function | ExprState(f,a,k,e,m) -> ignore(diagnose_stuck_expr p ge w f a k e m) | _ -> () -(* Exploration *) +(* Execution of a single step. Return list of triples + (reduction rule, next state, next world). *) -let do_step p prog ge time (s, w) = - if !trace >= 2 then - fprintf p "@[Time %d: %a@]@." time print_state (prog, ge, s); +let do_step p prog ge time s w = match Cexec.at_final_state s with | Some r -> if !trace >= 1 then @@ -513,89 +498,71 @@ let do_step p prog ge time (s, w) = end | None -> let l = Cexec.do_step ge do_external_function do_inline_assembly w s in - if l = [] || List.exists (fun (t,s) -> s = Stuckstate) l then begin + if l = [] + || List.exists (fun (Cexec.TR(r,t,s)) -> s = Stuckstate) l + then begin pp_set_max_boxes p 1000; fprintf p "@[Stuck state: %a@]@." print_state (prog, ge, s); diagnose_stuck_state p ge w s; fprintf p "ERROR: Undefined behavior@."; exit 126 end else begin - List.map (fun (t, s') -> (s', do_events p ge time w t)) l + List.map (fun (Cexec.TR(r, t, s')) -> (r, s', do_events p ge time w t)) l end -let rec explore_one p prog ge time sw = - let succs = do_step p prog ge time sw in +(* Exploration of a single execution. *) + +let rec explore_one p prog ge time s w = + if !trace >= 2 then + fprintf p "@[Time %d:@ %a@]@." time print_state (prog, ge, s); + let succs = do_step p prog ge time s w in if succs <> [] then begin - let sw' = + let (r, s', w') = match !mode with | First -> List.hd succs | Random -> List.nth succs (Random.int (List.length succs)) | All -> assert false in - explore_one p prog ge (time + 1) sw' + if !trace >= 2 then + fprintf p "--[%s]-->@." (camlstring_of_coqstring r); + explore_one p prog ge (time + 1) s' w' end -(* A priority queue structure where the priority is inversely proportional - to the memory nextblock. *) - -module PrioQueue = struct - - type elt = int * StateSet.elt - - type queue = Empty | Node of elt * queue * queue - - let empty = Empty - - let singleton elt = Node(elt, Empty, Empty) - - let higher_prio (time1, (s1, w1)) (time2, (s2, w2)) = - P.lt (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock - - let rec insert queue elt = - match queue with - | Empty -> Node(elt, Empty, Empty) - | Node(e, left, right) -> - if higher_prio elt e - then Node(elt, insert right e, left) - else Node(e, insert right elt, left) - - let rec remove_top = function - | Empty -> assert false - | Node(elt, left, Empty) -> left - | Node(elt, Empty, right) -> right - | Node(elt, (Node(lelt, _, _) as left), - (Node(relt, _, _) as right)) -> - if higher_prio lelt relt - then Node(lelt, remove_top left, right) - else Node(relt, left, remove_top right) - - let extract = function - | Empty -> None - | Node(elt, _, _) as queue -> Some(elt, remove_top queue) - - (* Return true if all elements of queue have strictly lower priority - than elt. *) - let dominate elt queue = - match queue with - | Empty -> true - | Node(e, _, _) -> higher_prio elt e -end - -let rec explore_all p prog ge seen queue = - match PrioQueue.extract queue with - | None -> () - | Some((time, sw) as tsw, queue') -> - if StateSet.mem sw seen then - explore_all p prog ge seen queue' - else - let succs = - List.rev_map (fun sw -> (time + 1, sw)) (do_step p prog ge time sw) in - let queue'' = List.fold_left PrioQueue.insert queue' succs in - let seen' = StateSet.add sw seen in - let seen'' = - if PrioQueue.dominate tsw queue'' - then purge_seen (mem_state (fst sw)).Mem.nextblock seen' - else seen' in - explore_all p prog ge seen'' queue'' +(* Exploration of all possible executions. *) + +let rec explore_all p prog ge time states = + if !trace >= 2 then begin + List.iter + (fun (n, s, w) -> + fprintf p "@[State %d.%d: @ %a@]@." + time n print_state (prog, ge, s)) + states + end; + let rec explore_next nextstates seen numseen = function + | [] -> + List.rev nextstates + | (n, s, w) :: states -> + add_reducts nextstates seen numseen states n (do_step p prog ge time s w) + + and add_reducts nextstates seen numseen states n = function + | [] -> + explore_next nextstates seen numseen states + | (r, s', w') :: reducts -> + let (n', nextstates', seen', numseen') = + try + (StateMap.find s' seen, nextstates, seen, numseen) + with Not_found -> + (numseen, + (numseen, s', w') :: nextstates, + StateMap.add s' numseen seen, + numseen + 1) in + if !trace >= 2 then begin + fprintf p "Transition state %d.%d --[%s]--> state %d.%d@." + time n (camlstring_of_coqstring r) (time + 1) n' + end; + add_reducts nextstates' seen' numseen' states n reducts + in + let nextstates = explore_next [] StateMap.empty 1 states in + if nextstates <> [] then explore_all p prog ge (time + 1) nextstates (* The variant of the source program used to build the world for executing events. @@ -680,7 +647,6 @@ let execute prog = | Some(ge, s) -> match !mode with | First | Random -> - explore_one p prog1 ge 0 (s, world wge wm) + explore_one p prog1 ge 0 s (world wge wm) | All -> - explore_all p prog1 ge StateSet.empty - (PrioQueue.singleton (0, (s, world wge wm))) + explore_all p prog1 ge 0 [(1, s, world wge wm)] -- cgit