From 453068fa5340134b6efba7f759a265f702831133 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 2 Dec 2020 13:50:00 -0800 Subject: [PATCH] [sledge] Revise Control flow exploration algorithm Summary: Revise the control-flow exploration scheduling algorithm to fix several issues. The main difference is to change the priority queue to keep the control edges on the frontier of exploration in sync with the states that are waiting to be propagated. This fixes several sorts of issue where the decision of which control and state joins to perform was unexpected / wrong. Part of keeping the frontier edges and waiting states in sync is that the waiting states are associated not only with a destination block, but the stack of that block. This fixes several issues. Combined, these changes lead to the algorithm only attempting joins for which the pointwise max join on depth maps is correct (with the caveat of no mathematical proof yet). Reviewed By: jvillard Differential Revision: D25196733 fbshipit-source-id: db007fe1f --- sledge/cli/domain_itv.ml | 3 +- sledge/nonstdlib/NS.mli | 8 +- sledge/nonstdlib/NS0.ml | 8 +- sledge/src/control.ml | 177 ++++++++++++++++++++---------- sledge/src/domain_intf.ml | 2 +- sledge/src/domain_relation.ml | 3 +- sledge/src/domain_sh.ml | 2 +- sledge/src/domain_unit.ml | 2 +- sledge/src/domain_used_globals.ml | 2 +- 9 files changed, 141 insertions(+), 66 deletions(-) diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml index 92dae6d87..0c854dbcd 100644 --- a/sledge/cli/domain_itv.ml +++ b/sledge/cli/domain_itv.ml @@ -16,9 +16,10 @@ let equal_apron_typ = (** Apron-managed map from variables to intervals *) type t = Box.t Abstract1.t +let equal : t -> t -> bool = Poly.equal +let compare : t -> t -> int = Poly.compare let man = lazy (Box.manager_alloc ()) let join l r = Some (Abstract1.join (Lazy.force man) l r) -let equal l r = Abstract1.is_eq (Lazy.force man) l r let is_false x = Abstract1.is_bottom (Lazy.force man) x let bindings (itv : t) = diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli index a214a8942..08518cc2a 100644 --- a/sledge/nonstdlib/NS.mli +++ b/sledge/nonstdlib/NS.mli @@ -158,7 +158,13 @@ module Set = Set module Map = Map module Multiset = Multiset module Bijection = CCBijection [@@warning "-49"] -module FHeap = Fheap [@@warning "-49"] + +module FHeap : sig + include module type of Fheap + + val remove_top_exn : 'a t -> 'a t +end + module HashSet = HashSet module HashTable = HashTable module HashQueue = Core_kernel.Hash_queue diff --git a/sledge/nonstdlib/NS0.ml b/sledge/nonstdlib/NS0.ml index 0d7bbd075..4d8887d29 100644 --- a/sledge/nonstdlib/NS0.ml +++ b/sledge/nonstdlib/NS0.ml @@ -131,7 +131,13 @@ end module Pair = Containers.Pair module Bijection = CCBijection [@@warning "-49"] -module FHeap = Fheap [@@warning "-49"] + +module FHeap = struct + include Fheap + + let remove_top_exn h = snd (pop_exn h) +end + module HashQueue = Core_kernel.Hash_queue (** Input / Output *) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 6f9b98665..a1508d492 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -18,6 +18,9 @@ type exec_opts = module Make (Dom : Domain_intf.Dom) = struct module Stack : sig type t + + val pp : t pp + type as_inlined_location = t [@@deriving compare, sexp_of] val empty : t @@ -50,6 +53,15 @@ module Make (Dom : Domain_intf.Dom) = struct | Empty [@@deriving sexp_of] + let rec pp ppf = function + | Return {recursive= false; dst; stk= s} -> + Format.fprintf ppf "R#%i%a" dst.dst.sort_index pp s + | Return {recursive= true; dst; stk= s} -> + Format.fprintf ppf "R↑#%i%a" dst.dst.sort_index pp s + | Throw (dst, s) -> + Format.fprintf ppf "T#%i%a" dst.dst.sort_index pp s + | Empty -> () + type as_inlined_location = t [@@deriving sexp_of] (* Treat a stack as a code location in a hypothetical expansion of the @@ -78,23 +90,11 @@ module Make (Dom : Domain_intf.Dom) = struct | _, Throw _ -> 1 | Empty, Empty -> 0 - let rec print_abbrev fs = function - | Return {recursive= false; stk= s} -> - print_abbrev fs s ; - Format.pp_print_char fs 'R' - | Return {recursive= true; stk= s} -> - print_abbrev fs s ; - Format.pp_print_string fs "R↑" - | Throw (_, s) -> - print_abbrev fs s ; - Format.pp_print_char fs 'T' - | Empty -> () - let invariant s = let@ () = Invariant.invariant [%here] s [%sexp_of: t] in match s with | Return _ | Throw (_, Return _) | Empty -> () - | Throw _ -> fail "malformed stack: %a" print_abbrev s () + | Throw _ -> fail "malformed stack: %a" pp s () let empty = Empty |> check invariant @@ -108,7 +108,7 @@ module Make (Dom : Domain_intf.Dom) = struct |> check invariant let push_call (Llair.{return; throw} as call) ~bound from_call stk = - [%Trace.call fun {pf} -> pf "%a" print_abbrev stk] + [%Trace.call fun {pf} -> pf "%a" pp stk] ; let rec count_f_in_stack acc f = function | Return {stk= next_frame; dst= dest_block} -> @@ -184,7 +184,7 @@ module Make (Dom : Domain_intf.Dom) = struct module Depths = struct module M = Map.Make (Edge) - type t = int M.t + type t = int M.t [@@deriving compare, sexp_of] let empty = M.empty let find = M.find @@ -196,62 +196,116 @@ module Make (Dom : Domain_intf.Dom) = struct | `Both (d1, d2) -> Some (Int.max d1 d2) ) end - type priority = int * Edge.t [@@deriving compare] - type priority_queue = priority FHeap.t - type waiting_states = (Dom.t * Depths.t) list Llair.Block.Map.t - type t = priority_queue * waiting_states * int - type x = Depths.t -> t -> t + module PrioQueue : sig + (** an edge at a depth with the domain and depths state it yielded *) + type elt = {depth: int; edge: Edge.t; state: Dom.t; depths: Depths.t} + + type t + + val pp : t pp + + val create : unit -> t + (** create an empty queue *) + + val add : elt -> t -> t + (** add an element *) + + val remove : elt -> t -> t + (** remove an element *) - let empty_waiting_states : waiting_states = Llair.Block.Map.empty - let pp_priority fs (n, e) = Format.fprintf fs "%i: %a" n Edge.pp e + val pop : t -> (elt * elt list * t) option + (** the top element, the other elements with the same destination, the + queue without the top element *) + end = struct + type elt = {depth: int; edge: Edge.t; state: Dom.t; depths: Depths.t} + [@@deriving compare, sexp_of] - let pp fs pq = - Format.fprintf fs "@[%a@]" - (List.pp " ::@ " pp_priority) - (FHeap.to_list pq) + module Elts = Set.Make (struct + type t = elt [@@deriving compare, sexp_of] + end) + + type t = {queue: elt FHeap.t; removed: Elts.t} + + let pp_elt ppf {depth; edge} = + Format.fprintf ppf "%i: %a" depth Edge.pp edge + + let pp ppf {queue; removed} = + let rev_elts = + FHeap.fold queue ~init:[] ~f:(fun rev_elts elt -> + if Elts.mem elt removed then rev_elts else elt :: rev_elts ) + in + Format.fprintf ppf "@[%a@]" (List.pp " ::@ " pp_elt) + (List.rev rev_elts) + + let create () = + {queue= FHeap.create ~cmp:compare_elt; removed= Elts.empty} + + let add elt {queue; removed} = + let removed' = Elts.remove elt removed in + if removed' == removed then {queue= FHeap.add queue elt; removed} + else {queue; removed= removed'} + + let remove elt {queue; removed} = + {queue; removed= Elts.add elt removed} + + let rec pop {queue; removed} = + let* top, queue = FHeap.pop queue in + let removed' = Elts.remove top removed in + if removed' != removed then pop {queue; removed= removed'} + else + let elts = + FHeap.fold queue ~init:[] ~f:(fun elts elt -> + if + Llair.Block.equal top.edge.dst elt.edge.dst + && not (Elts.mem elt removed) + then elt :: elts + else elts ) + in + Some (top, elts, {queue; removed}) + end + + type t = PrioQueue.t * int + type x = Depths.t -> t -> t let skip _ w = w let seq x y d w = y d (x d w) - let add ?prev ~retreating stk state curr depths ((pq, ws, bound) as work) - = + let add ?prev ~retreating stk state curr depths (queue, bound) = let edge = {Edge.dst= curr; src= prev; stk} in let depth = Option.value (Depths.find edge depths) ~default:0 in let depth = if retreating then depth + 1 else depth in - if depth > bound then ( + if depth <= bound then ( + [%Trace.info + "@[<6>enqueue %i: %a [%a]@ | %a@]" depth Edge.pp edge Stack.pp + edge.stk PrioQueue.pp queue] ; + let depths = Depths.add ~key:edge ~data:depth depths in + (PrioQueue.add {depth; edge; state; depths} queue, bound) ) + else ( [%Trace.info "prune: %i: %a" depth Edge.pp edge] ; Report.hit_bound bound ; - work ) - else - let pq = FHeap.add pq (depth, edge) in - [%Trace.info "@[<6>enqueue %i: %a@ | %a@]" depth Edge.pp edge pp pq] ; - let depths = Depths.add ~key:edge ~data:depth depths in - let ws = - Llair.Block.Map.add_multi ~key:curr ~data:(state, depths) ws - in - (pq, ws, bound) + (queue, bound) ) let init state curr bound = add ~retreating:false Stack.empty state curr Depths.empty - (FHeap.create ~cmp:compare_priority, empty_waiting_states, bound) - - let rec run ~f (pq0, ws, bnd) = - match FHeap.pop pq0 with - | Some ((_, ({Edge.dst; stk} as edge)), pq) -> ( - match Llair.Block.Map.find_and_remove dst ws with - | Some (q :: qs, ws) -> - let join (qa, da) (q, d) = (Dom.join q qa, Depths.join d da) in - let skipped, (qs, depths) = - List.fold qs ([], q) ~f:(fun curr (skipped, joined) -> - match join curr joined with - | Some joined, depths -> (skipped, (joined, depths)) - | None, _ -> (curr :: skipped, joined) ) - in - let ws = Llair.Block.Map.add_exn ~key:dst ~data:skipped ws in - run ~f (f stk qs dst depths (pq, ws, bnd)) - | _ -> - [%Trace.info "done: %a" Edge.pp edge] ; - run ~f (pq, ws, bnd) ) + (PrioQueue.create (), bound) + + let rec run ~f (queue, bound) = + match PrioQueue.pop queue with + | Some ({depth; edge; state; depths}, elts, queue) -> + [%Trace.info + "@[<6>dequeue %i: %a [%a]@ | %a@]" depth Edge.pp edge Stack.pp + edge.stk PrioQueue.pp queue] ; + let state, depths, queue = + List.fold elts (state, depths, queue) + ~f:(fun elt (state, depths, queue) -> + match Dom.join elt.state state with + | Some state -> + let depths = Depths.join elt.depths depths in + let queue = PrioQueue.remove elt queue in + (state, depths, queue) + | None -> (state, depths, queue) ) + in + run ~f (f edge.stk state edge.dst depths (queue, bound)) | None -> [%Trace.info "queue empty"] ; () @@ -466,7 +520,14 @@ module Make (Dom : Domain_intf.Dom) = struct -> Llair.block -> Work.x = fun opts pgm stk state block -> - [%Trace.info "exec block %%%s" block.lbl] ; + [%trace] + ~call:(fun {pf} -> + pf "#%i %%%s in %a" block.sort_index block.lbl Llair.Function.pp + block.parent.name ) + ~retn:(fun {pf} _ -> + pf "#%i %%%s in %a" block.sort_index block.lbl Llair.Function.pp + block.parent.name ) + @@ fun () -> match Iter.fold_result ~f:exec_inst (IArray.to_iter block.cmnd) state with diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml index 851c1323a..6a79c8a6b 100644 --- a/sledge/src/domain_intf.ml +++ b/sledge/src/domain_intf.ml @@ -7,7 +7,7 @@ (** Abstract Domain *) module type Dom = sig - type t [@@deriving equal, sexp_of] + type t [@@deriving compare, equal, sexp_of] val pp : t pp val report_fmt_thunk : t -> Format.formatter -> unit diff --git a/sledge/src/domain_relation.ml b/sledge/src/domain_relation.ml index 524fdee4b..88e7c64ce 100644 --- a/sledge/src/domain_relation.ml +++ b/sledge/src/domain_relation.ml @@ -20,7 +20,8 @@ module type State_domain_sig = sig end module Make (State_domain : State_domain_sig) = struct - type t = State_domain.t * State_domain.t [@@deriving equal, sexp_of] + type t = State_domain.t * State_domain.t + [@@deriving compare, equal, sexp_of] let embed b = (b, b) diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 73cd7ae5d..48acfd8f2 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -10,7 +10,7 @@ module X = Llair_to_Fol open Fol -type t = Sh.t [@@deriving equal, sexp] +type t = Sh.t [@@deriving compare, equal, sexp] let pp fs q = Format.fprintf fs "@[{ %a@ }@]" Sh.pp q let report_fmt_thunk = Fun.flip pp diff --git a/sledge/src/domain_unit.ml b/sledge/src/domain_unit.ml index d02efde6b..0c5f11f06 100644 --- a/sledge/src/domain_unit.ml +++ b/sledge/src/domain_unit.ml @@ -7,7 +7,7 @@ (** "Unit" abstract domain *) -type t = unit [@@deriving equal, sexp] +type t = unit [@@deriving compare, equal, sexp] let pp fs () = Format.pp_print_string fs "()" let report_fmt_thunk () fs = pp fs () diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml index 4050a4555..ceb23cec0 100644 --- a/sledge/src/domain_used_globals.ml +++ b/sledge/src/domain_used_globals.ml @@ -7,7 +7,7 @@ (** Used-globals abstract domain *) -type t = Llair.Global.Set.t [@@deriving equal, sexp] +type t = Llair.Global.Set.t [@@deriving compare, equal, sexp] let pp = Llair.Global.Set.pp let report_fmt_thunk = Fun.flip pp