From 20eea14b1c678722642da5c22afd6e87b6cdf686 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Mar 2013 17:26:30 +0000 Subject: Improving the performance of exhaustive exploration (mode -all): - Re-share states even at different times - Faster comparison between states, giving priority to the mem nextblock git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2138 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Interp.ml | 130 +++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 112 insertions(+), 18 deletions(-) (limited to 'driver') diff --git a/driver/Interp.ml b/driver/Interp.ml index 3be9748..b7971ed 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -140,13 +140,14 @@ let print_state p (prog, ge, s) = (* Comparing memory states *) -let compare_mem m1 m2 = (* should permissions be taken into account? *) - Pervasives.compare (m1.Mem.nextblock, m1.Mem.mem_contents) - (m2.Mem.nextblock, m2.Mem.mem_contents) +let compare_mem m1 m2 = + (* assumes nextblocks were already compared equal *) + (* should permissions be taken into account? *) + Pervasives.compare m1.Mem.mem_contents m2.Mem.mem_contents (* Comparing continuations *) -let some_expr = Evar(P.one, Tvoid) +let some_expr = Eval(Vptr(Mem.nullptr, Int.zero), Tvoid) let rank_cont = function | Kstop -> 0 @@ -214,10 +215,19 @@ let rank_state = function | ExprState _ -> 1 | Callstate _ -> 2 | Returnstate _ -> 3 - | Stuckstate -> 4 + | 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 + | Stuckstate -> assert false let compare_state s1 s2 = if s1 == s2 then 0 else + let c = Z.compare (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock in + if c <> 0 then c else begin match s1, s2 with | State(f1,s1,k1,e1,m1), State(f2,s2,k2,e2,m2) -> let c = compare (f1,s1,e1) (f2,s2,e2) in if c <> 0 then c else @@ -237,6 +247,9 @@ let compare_state s1 s2 = compare_mem m1 m2 | _, _ -> compare (rank_state s1) (rank_state s2) + end + +(* Sets of states already explored *) module StateSet = Set.Make(struct @@ -244,6 +257,20 @@ module StateSet = let compare (s1,w1) (s2,w2) = compare_state s1 s2 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 Z.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 ge m id ofs = @@ -430,12 +457,12 @@ let do_step p prog ge time (s, w) = fprintf p "@[Time %d: %a@]@." time print_state (prog, ge, s); match Cexec.at_final_state s with | Some r -> - if !trace >= 1 then begin + if !trace >= 1 then fprintf p "Time %d: program terminated (exit code = %ld)@." time (camlint_of_coqint r); - [] - end else begin - exit (Int32.to_int (camlint_of_coqint r)) + begin match !mode with + | All -> [] + | First | Random -> exit (Int32.to_int (camlint_of_coqint r)) end | None -> let l = Cexec.do_step ge w s in @@ -449,18 +476,80 @@ let do_step p prog ge time (s, w) = List.map (fun (t, s') -> (s', do_events p ge time w t)) l end -let rec explore p prog ge time ss = - let succs = - StateSet.fold (fun sw l -> do_step p prog ge time sw @ l) ss [] in +let rec explore_one p prog ge time sw = + let succs = do_step p prog ge time sw in if succs <> [] then begin - let ss' = + let sw' = match !mode with - | First -> StateSet.singleton (List.hd succs) - | Random -> StateSet.singleton (List.nth succs (Random.int (List.length succs))) - | All -> List.fold_right StateSet.add succs StateSet.empty in - explore p prog ge (time + 1) ss' + | 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' 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)) = + Z.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'' + (* The variant of the source program used to build the world for executing events. Volatile variables are turned into non-volatile ones, so that @@ -541,4 +630,9 @@ let execute prog = | None -> fprintf p "ERROR: Initial state undefined@." | Some(ge, s) -> - explore p prog1 ge 0 (StateSet.singleton (s, world wge wm)) + match !mode with + | First | Random -> + 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))) -- cgit v1.2.3