diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-19 16:24:28 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-19 16:24:28 +0100 |
commit | e51ffb6c1d9411515facc5e97a4e8dba5d8b55ab (patch) | |
tree | 80a7fc8212d28712365082e1a2a2d0fa28cedad3 /driver | |
parent | c130f4936bad11fd6dab3a5d142b870d2a5f650c (diff) | |
parent | b0eb1dfc9fd7b15c556c49101390d882b0f00f8a (diff) | |
download | compcert-e51ffb6c1d9411515facc5e97a4e8dba5d8b55ab.tar.gz compcert-e51ffb6c1d9411515facc5e97a4e8dba5d8b55ab.zip |
Merge branch 'master' into no-shell
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Commandline.ml | 11 | ||||
-rw-r--r-- | driver/Commandline.mli | 3 | ||||
-rw-r--r-- | driver/Driver.ml | 56 | ||||
-rw-r--r-- | driver/Interp.ml | 180 |
4 files changed, 113 insertions, 137 deletions
diff --git a/driver/Commandline.ml b/driver/Commandline.ml index bc095af6..0a2c8fca 100644 --- a/driver/Commandline.ml +++ b/driver/Commandline.ml @@ -52,7 +52,7 @@ let rec find_action text = function | (pat, act) :: rem -> if match_pattern text pat then Some act else find_action text rem -let parse_array spec usage argv first last = +let parse_array spec argv first last = (* Split the spec into Exact patterns (in a hashtable) and other patterns *) let exact_cases = (Hashtbl.create 29 : (string, action) Hashtbl.t) in let rec split_spec = function @@ -69,10 +69,7 @@ let parse_array spec usage argv first last = with Not_found -> find_action s inexact_cases in match optact with | None -> - if s <> "-help" && s <> "--help" - then eprintf "Unknown argument `%s'\n" s - else printf "%s" usage; - exit 2 + eprintf "Unknown argument `%s'\n" s; exit 2 | Some(Set r) -> r := true; parse (i+1) | Some(Unset r) -> @@ -101,5 +98,5 @@ let parse_array spec usage argv first last = end in parse first -let parse_cmdline spec usage = - parse_array spec usage Sys.argv 1 (Array.length Sys.argv - 1) +let parse_cmdline spec = + parse_array spec Sys.argv 1 (Array.length Sys.argv - 1) diff --git a/driver/Commandline.mli b/driver/Commandline.mli index 7a18905f..79786678 100644 --- a/driver/Commandline.mli +++ b/driver/Commandline.mli @@ -34,8 +34,7 @@ type action = | String of (string -> unit) (** read next arg as a string, call function *) | Integer of (int -> unit) (** read next arg as an int, call function *) -val parse_cmdline: - (pattern * action) list -> string (* usage string *) -> unit +val parse_cmdline: (pattern * action) list -> unit (* Note on precedence: [Exact] patterns are tried first, then the other patterns are tried in the order in which they appear in the list. *) diff --git a/driver/Driver.ml b/driver/Driver.ml index 14ce11f4..d22dd77c 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -130,7 +130,7 @@ let parse_c_file sourcename ifile = end; (* Conversion to Csyntax *) let csyntax = - match C2C.convertProgram ast with + match Timing.time "CompCert C generation" C2C.convertProgram ast with | None -> exit 2 | Some p -> p in flush stderr; @@ -466,6 +466,9 @@ Interpreter mode: -all Simulate all possible execution orders " +let print_usage_and_exit _ = + printf "%s" usage_string; exit 0 + let language_support_options = [ option_fbitfields; option_flongdouble; option_fstruct_return; option_fvararg_calls; option_funprototyped; @@ -485,26 +488,9 @@ let cmdline_actions = let f_opt name ref = [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in [ -(* File arguments *) - Suffix ".c", Self (fun s -> - push_action process_c_file s; incr num_source_files); - Suffix ".i", Self (fun s -> - push_action process_i_file s; incr num_source_files); - Suffix ".p", Self (fun s -> - push_action process_i_file s; incr num_source_files); - Suffix ".cm", Self (fun s -> - push_action process_cminor_file s; incr num_source_files); - Suffix ".s", Self (fun s -> - push_action process_s_file s; incr num_source_files); - Suffix ".S", Self (fun s -> - push_action process_S_file s; incr num_source_files); - Suffix ".o", Self push_linker_arg; - Suffix ".a", Self push_linker_arg; - (* GCC compatibility: .o.ext files are also object files *) - _Regexp ".*\\.o\\.", Self push_linker_arg; - (* GCC compatibility: .h files can be preprocessed with -E *) - Suffix ".h", Self (fun s -> - push_action process_h_file s; incr num_source_files); +(* Getting help *) + Exact "-help", Self print_usage_and_exit; + Exact "--help", Self print_usage_and_exit; (* Processing options *) Exact "-c", Set option_c; Exact "-E", Set option_E; @@ -583,6 +569,32 @@ let cmdline_actions = (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) + @ [ +(* Catch options that are not handled *) + Prefix "-", Self (fun s -> + eprintf "Unknown option `%s'\n" s; exit 2); +(* File arguments *) + Suffix ".c", Self (fun s -> + push_action process_c_file s; incr num_source_files); + Suffix ".i", Self (fun s -> + push_action process_i_file s; incr num_source_files); + Suffix ".p", Self (fun s -> + push_action process_i_file s; incr num_source_files); + Suffix ".cm", Self (fun s -> + push_action process_cminor_file s; incr num_source_files); + Suffix ".s", Self (fun s -> + push_action process_s_file s; incr num_source_files); + Suffix ".S", Self (fun s -> + push_action process_S_file s; incr num_source_files); + Suffix ".o", Self push_linker_arg; + Suffix ".a", Self push_linker_arg; + (* GCC compatibility: .o.ext files and .so files are also object files *) + _Regexp ".*\\.o\\.", Self push_linker_arg; + Suffix ".so", Self push_linker_arg; + (* GCC compatibility: .h files can be preprocessed with -E *) + Suffix ".h", Self (fun s -> + push_action process_h_file s; incr num_source_files); + ] let _ = try @@ -600,7 +612,7 @@ let _ = end; Builtins.set C2C.builtins; CPragmas.initialize(); - parse_cmdline cmdline_actions usage_string; + parse_cmdline cmdline_actions; let nolink = !option_c || !option_S || !option_E || !option_interp in if nolink && !option_o <> None && !num_source_files >= 2 then begin eprintf "Ambiguous '-o' option (multiple source files)\n"; diff --git a/driver/Interp.ml b/driver/Interp.ml index 9bb9d237..2725dbfe 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -122,22 +122,22 @@ let print_val_list p vl = let print_state p (prog, ge, s) = match s with | State(f, s, k, e, m) -> - PrintCsyntax.print_pointer_hook := print_pointer ge 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) -> - PrintCsyntax.print_pointer_hook := print_pointer ge 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) -> - PrintCsyntax.print_pointer_hook := print_pointer ge Maps.PTree.empty; + 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) -> - PrintCsyntax.print_pointer_hook := print_pointer ge Maps.PTree.empty; + PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv Maps.PTree.empty; fprintf p "returning@ %a" print_val res | Stuckstate -> @@ -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 = @@ -389,7 +375,7 @@ let convert_external_arg ge v t = | Vsingle f, AST.Tsingle -> Some (EVsingle f) | Vlong n, AST.Tlong -> Some (EVlong n) | Vptr(b, ofs), AST.Tint -> - Genv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs)) + Senv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs)) | _, _ -> None let rec convert_external_args ge vl tl = @@ -422,20 +408,20 @@ and world_io ge m id args = None and world_vload ge m chunk id ofs = - Genv.find_symbol ge id >>= fun b -> + Genv.find_symbol ge.genv_genv id >>= fun b -> Mem.load chunk m b ofs >>= fun v -> Cexec.eventval_of_val ge v (type_of_chunk chunk) >>= fun ev -> Some(ev, world ge m) and world_vstore ge m chunk id ofs ev = - Genv.find_symbol ge id >>= fun b -> + Genv.find_symbol ge.genv_genv id >>= fun b -> Cexec.val_of_eventval ge ev (type_of_chunk chunk) >>= fun v -> Mem.store chunk m b ofs v >>= fun m' -> Some(world ge m') let do_event p ge time w ev = if !trace >= 1 then - fprintf p "@[<hov 2>Time %d: observable event:@ @[<hov 2>%a@]@]@." + fprintf p "@[<hov 2>Time %d: observable event:@ %a@]@." time print_event ev; (* Return new world after external action *) match ev with @@ -479,7 +465,7 @@ let diagnose_stuck_expr p ge w f a kont e m = 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 - PrintCsyntax.print_pointer_hook := print_pointer ge e; + PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e; fprintf p "@[<hov 2>Stuck subexpression:@ %a@]@." PrintCsyntax.print_expr a; true @@ -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 "@[<hov 2>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 "@[<hov 2>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 "@[<hov 2>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 "@[<hov 2>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. @@ -633,7 +600,9 @@ let change_main_function p old_main old_main_ty = 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; - prog_public = p.prog_public } + prog_public = p.prog_public; + prog_types = p.prog_types; + prog_comp_env = p.prog_comp_env } let rec find_main_function name = function | [] -> None @@ -667,8 +636,8 @@ let execute prog = | None -> exit 126 | Some prog1 -> let wprog = world_program prog1 in - let wge = Genv.globalenv wprog in - match Genv.init_mem wprog with + let wge = globalenv wprog in + match Genv.init_mem (program_of_program wprog) with | None -> fprintf p "ERROR: World memory state undefined@."; exit 126 | Some wm -> @@ -678,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)] |