[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

@@ -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) =

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

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 *)

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]
+    module PrioQueue : sig
-    type priority_queue = priority FHeap.t
+      (** an edge at a depth with the domain and depths state it yielded *)
-    type waiting_states = (Dom.t * Depths.t) list Llair.Block.Map.t
+      type elt = {depth: int; edge: Edge.t; state: Dom.t; depths: Depths.t}
-    type t = priority_queue * waiting_states * int
+
-    type x = Depths.t -> t -> 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
+      val pop : t -> (elt * elt list * t) option
-    let pp_priority fs (n, e) = Format.fprintf fs "%i: %a" n Edge.pp e
+      (** 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 =
+      module Elts = Set.Make (struct
-      Format.fprintf fs "@[%a@]"
+        type t = elt [@@deriving compare, sexp_of]
-        (List.pp " ::@ " pp_priority)
+      end)
-        (FHeap.to_list pq)
+
+      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 )
+        (queue, bound) )
-      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)
 
     let init state curr bound =
       add ~retreating:false Stack.empty state curr Depths.empty
-        (FHeap.create ~cmp:compare_priority, empty_waiting_states, bound)
+        (PrioQueue.create (), bound)
-
+
-    let rec run ~f (pq0, ws, bnd) =
+    let rec run ~f (queue, bound) =
-      match FHeap.pop pq0 with
+      match PrioQueue.pop queue with
-      | Some ((_, ({Edge.dst; stk} as edge)), pq) -> (
+      | Some ({depth; edge; state; depths}, elts, queue) ->
-        match Llair.Block.Map.find_and_remove dst ws with
+          [%Trace.info
-        | Some (q :: qs, ws) ->
+            "@[<6>dequeue %i: %a [%a]@ | %a@]" depth Edge.pp edge Stack.pp
-            let join (qa, da) (q, d) = (Dom.join q qa, Depths.join d da) in
+              edge.stk PrioQueue.pp queue] ;
-            let skipped, (qs, depths) =
+          let state, depths, queue =
-              List.fold qs ([], q) ~f:(fun curr (skipped, joined) ->
+            List.fold elts (state, depths, queue)
-                  match join curr joined with
+              ~f:(fun elt (state, depths, queue) ->
-                  | Some joined, depths -> (skipped, (joined, depths))
+                match Dom.join elt.state state with
-                  | None, _ -> (curr :: skipped, joined) )
+                | Some state ->
-            in
+                    let depths = Depths.join elt.depths depths in
-            let ws = Llair.Block.Map.add_exn ~key:dst ~data:skipped ws in
+                    let queue = PrioQueue.remove elt queue in
-            run ~f (f stk qs dst depths (pq, ws, bnd))
+                    (state, depths, queue)
-        | _ ->
+                | None -> (state, depths, queue) )
-            [%Trace.info "done: %a" Edge.pp edge] ;
+          in
-            run ~f (pq, ws, bnd) )
+          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

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

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)
 

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

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 ()

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