[sledge] Add option to apply used-globals as pre-analysis

Summary:
This diff adds a "-prenalyze-globals" flag to all analyze targets
which, when set, computes used-globals sets for all reachable
functions and then uses that information to track only relevant
global variables at calls in the main analysis.

Reviewed By: jberdine, jvillard

Differential Revision: D17526746

fbshipit-source-id: 1a114285c

sledge/sledge-help.txt

@@ -56,6 +56,7 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s
   [-margin <cols>]        wrap debug tracing at <cols> columns
   [-modules <file>]       write list of bitcode files to <file>, or to standard
                           output if <file> is `-`
+  [-preanalyze-globals]   pre-analyze global variables used by each function
   [-skip-throw]           do not explore past throwing an exception
   [-trace <spec>]         enable debug tracing
   [-help]                 print this help text and exit
@@ -136,6 +137,7 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo
   [-fuzzer]               add a harness for libFuzzer targets
   [-llair-output <file>]  write generated LLAIR to <file>
   [-margin <cols>]        wrap debug tracing at <cols> columns
+  [-preanalyze-globals]   pre-analyze global variables used by each function
   [-skip-throw]           do not explore past throwing an exception
   [-trace <spec>]         enable debug tracing
   [-help]                 print this help text and exit
@@ -178,6 +180,7 @@ The <input> file must be binary LLAIR, such as produced by `sledge translate`.
                          or "unit" (unit domain)
   [-function-summaries]  use function summaries (in development)
   [-margin <cols>]       wrap debug tracing at <cols> columns
+  [-preanalyze-globals]  pre-analyze global variables used by each function
   [-skip-throw]          do not explore past throwing an exception
   [-trace <spec>]        enable debug tracing
   [-help]                print this help text and exit

sledge/src/control.ml

@@ -9,7 +9,12 @@
 
     The analysis' semantics of control flow. *)
 
-type exec_opts = {bound: int; skip_throw: bool; function_summaries: bool}
+type exec_opts =
+  { bound: int
+  ; skip_throw: bool
+  ; function_summaries: bool
+  ; globals: [`Per_function of Var.Set.t Var.Map.t | `Declared of Var.Set.t]
+  }
 
 module Make (Dom : Domain_sig.Dom) = struct
   module Stack : sig
@@ -237,6 +242,23 @@ module Make (Dom : Domain_sig.Dom) = struct
       | None -> [%Trace.info "queue empty"] ; ()
   end
 
+  let used_globals : exec_opts -> Var.var -> Var.Set.t =
+   fun opts fn ->
+    [%Trace.call fun {pf} -> pf "%a" Var.pp fn]
+    ;
+    ( match opts.globals with
+    | `Declared set -> set
+    | `Per_function map -> (
+      match Map.find map fn with
+      | Some gs -> gs
+      | None ->
+          fail
+            "main analysis reached function %a that was not reached by \
+             used-globals pre-analysis "
+            Var.pp fn () ) )
+    |>
+    [%Trace.retn fun {pf} r -> pf "%a" Var.Set.pp r]
+
   let exec_jump stk state block Llair.{dst; retreating} =
     Work.add ~prev:block ~retreating stk state dst
 
@@ -253,7 +275,8 @@ module Make (Dom : Domain_sig.Dom) = struct
       if opts.function_summaries then Dom.dnf state else [state]
     in
     let domain_call =
-      Dom.call args areturn params (Set.add_option freturn locals) globals
+      Dom.call ~globals args areturn params
+        ~locals:(Set.add_option freturn locals)
     in
     List.fold ~init:Work.skip dnf_states ~f:(fun acc state ->
         match
@@ -295,40 +318,44 @@ module Make (Dom : Domain_sig.Dom) = struct
                 (List.pp "@," Dom.pp_summary)
                 data ) )]
 
-  let exec_return ~opts stk pre_state (block : Llair.block) exp globals =
+  let exec_return ~opts stk pre_state (block : Llair.block) exp =
     let Llair.{name; params; freturn; locals} = block.parent in
     [%Trace.call fun {pf} ->
       pf "from %a with pre_state %a" Var.pp name.var Dom.pp pre_state]
     ;
+    let summarize post_state =
+      if opts.function_summaries then (
+        let globals = used_globals opts name.var in
+        let function_summary, post_state =
+          Dom.create_summary ~locals post_state
+            ~formals:(Set.union (Var.Set.of_list params) globals)
+        in
+        Hashtbl.add_multi summary_table ~key:name.var ~data:function_summary ;
+        pp_st () ;
+        post_state )
+      else post_state
+    in
+    let exit_state =
+      match (freturn, exp) with
+      | Some freturn, Some return_val ->
+          Dom.exec_move pre_state freturn return_val
+      | None, None -> pre_state
+      | _ -> violates Llair.Func.invariant block.parent
+    in
     ( match Stack.pop_return stk with
     | Some (from_call, retn_site, stk) ->
-        let exit_state =
-          match (freturn, exp) with
-          | Some freturn, Some return_val ->
-              Dom.exec_move pre_state freturn return_val
-          | None, None -> pre_state
-          | _ -> violates Llair.Func.invariant block.parent
-        in
-        let post_state = Dom.post locals from_call exit_state in
-        let post_state =
-          if opts.function_summaries then (
-            let globals =
-              Var.Set.of_vector
-                (Vector.map globals ~f:(fun (g : Global.t) -> g.var))
-            in
-            let function_summary, post_state =
-              Dom.create_summary ~locals post_state
-                ~formals:(Set.union (Var.Set.of_list params) globals)
-            in
-            Hashtbl.add_multi summary_table ~key:name.var
-              ~data:function_summary ;
-            pp_st () ;
-            post_state )
-          else post_state
-        in
+        let post_state = summarize (Dom.post locals from_call exit_state) in
         let retn_state = Dom.retn params freturn from_call post_state in
         exec_jump stk retn_state block retn_site
-    | None -> Work.skip )
+    | None ->
+        (* Create and store a function summary for main *)
+        if
+          opts.function_summaries
+          && List.exists
+               (Config.find_list "entry-points")
+               ~f:(String.equal (Var.name name.var))
+        then summarize exit_state |> (ignore : Dom.t -> unit) ;
+        Work.skip )
     |>
     [%Trace.retn fun {pf} _ -> pf ""]
 
@@ -419,9 +446,9 @@ module Make (Dom : Domain_sig.Dom) = struct
                     exec_skip_func stk state block areturn return
                 | None ->
                     exec_call opts stk state block {call with callee}
-                      pgm.globals )
+                      (used_globals opts callee.name.var) )
                 |> Work.seq x ) )
-    | Return {exp} -> exec_return ~opts stk state block exp pgm.globals
+    | Return {exp} -> exec_return ~opts stk state block exp
     | Throw {exc} ->
         if opts.skip_throw then Work.skip
         else exec_throw stk state block exc
@@ -449,12 +476,13 @@ module Make (Dom : Domain_sig.Dom) = struct
     List.find_map entry_points ~f:(fun name ->
         Llair.Func.find pgm.functions (Var.program ~global:() name) )
     |> function
-    | Some {locals; params= []; entry} ->
+    | Some {name= {var}; locals; params= []; entry} ->
         Some
           (Work.init
              (fst
-                (Dom.call ~summaries:opts.function_summaries [] None []
-                   locals pgm.globals (Dom.init pgm.globals)))
+                (Dom.call ~summaries:opts.function_summaries
+                   ~globals:(used_globals opts var) [] None [] ~locals
+                   (Dom.init pgm.globals)))
              entry)
     | _ -> None
 
@@ -467,4 +495,10 @@ module Make (Dom : Domain_sig.Dom) = struct
     | None -> fail "no applicable harness" () )
     |>
     [%Trace.retn fun {pf} _ -> pf ""]
+
+  let compute_summaries opts pgm : Dom.summary list Var.Map.t =
+    assert opts.function_summaries ;
+    exec_pgm opts pgm ;
+    Hashtbl.fold summary_table ~init:Var.Map.empty ~f:(fun ~key ~data map ->
+        match data with [] -> map | _ -> Map.set map ~key ~data )
 end

sledge/src/control.mli

@@ -10,8 +10,12 @@
 type exec_opts =
   { bound: int  (** Loop/recursion unrolling bound *)
   ; skip_throw: bool  (** Treat throw as unreachable *)
-  ; function_summaries: bool  (** Use function summarisation *) }
+  ; function_summaries: bool  (** Use function summarisation *)
+  ; globals: [`Per_function of Var.Set.t Var.Map.t | `Declared of Var.Set.t]
+        (** Either a per-function used-globals map or a program-wide set *)
+  }
 
 module Make (Dom : Domain_sig.Dom) : sig
   val exec_pgm : exec_opts -> Llair.t -> unit
+  val compute_summaries : exec_opts -> Llair.t -> Dom.summary list Var.Map.t
 end

sledge/src/domain/domain_sig.ml

@@ -31,11 +31,11 @@ module type Dom = sig
 
   val call :
        summaries:bool
+    -> globals:Var.Set.t
     -> Exp.t list
     -> Var.t option
     -> Var.t list
-    -> Var.Set.t
-    -> Global.t vector
+    -> locals:Var.Set.t
     -> t
     -> t * from_call
 

sledge/src/domain/relation.ml

@@ -69,26 +69,22 @@ module Make (State_domain : State_domain_sig) = struct
 
   let recursion_beyond_bound = State_domain.recursion_beyond_bound
 
-  let call ~summaries actuals areturn formals locals globals_vec
+  let call ~summaries ~globals actuals areturn formals ~locals
       (entry, current) =
-    let globals =
-      Var.Set.of_vector
-        (Vector.map globals_vec ~f:(fun (g : Global.t) -> g.var))
-    in
-    ([%Trace.call fun {pf} ->
-       pf
-         "@[<v>@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \
-          globals: {@[%a@]}@ current: %a@]"
-         (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
-         (List.rev formals) Var.Set.pp locals Var.Set.pp globals
-         State_domain.pp current]
+    [%Trace.call fun {pf} ->
+      pf
+        "@[<v>@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \
+         globals: {@[%a@]}@ current: %a@]"
+        (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
+        (List.rev formals) Var.Set.pp locals Var.Set.pp globals
+        State_domain.pp current]
     ;
     let caller_current, state_from_call =
-      State_domain.call ~summaries actuals areturn formals locals
-        globals_vec current
+      State_domain.call ~summaries ~globals actuals areturn formals ~locals
+        current
     in
     ( (caller_current, caller_current)
-    , {state_from_call; caller_entry= entry} ))
+    , {state_from_call; caller_entry= entry} )
     |>
     [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln]
 

sledge/src/domain/unit.ml

@@ -22,7 +22,7 @@ let exec_intrinsic ~skip_throw:_ _ _ _ _ : (t, unit) result option = None
 
 type from_call = unit [@@deriving compare, equal, sexp]
 
-let call ~summaries:_ _ _ _ _ _ _ = ((), ())
+let call ~summaries:_ ~globals:_ _ _ _ ~locals:_ _ = ((), ())
 let recursion_beyond_bound = `skip
 let post _ _ () = ()
 let retn _ _ _ _ = ()

sledge/src/domain/used_globals.ml

@@ -61,7 +61,7 @@ let exec_intrinsic ~skip_throw:_ st _ intrinsic actuals =
 type from_call = t [@@deriving sexp_of]
 
 (* Set abstract state to bottom (i.e. empty set) at function entry *)
-let call ~summaries:_ actuals _ _ _ _ st =
+let call ~summaries:_ ~globals:_ actuals _ _ ~locals:_ st =
   (empty, List.fold actuals ~init:st ~f:(fun s a -> used_globals ~init:s a))
 
 let resolve_callee lookup ptr st =

sledge/src/domain/used_globals.mli

@@ -7,4 +7,4 @@
 
 (** Used-globals abstract domain *)
 
-include Domain_sig.Dom
+include Domain_sig.Dom with type summary = Var.Set.t

sledge/src/llair/exp.ml

@@ -527,6 +527,7 @@ module Var = struct
     let empty = Set.empty (module T)
     let of_option = Option.fold ~f:Set.add ~init:empty
     let of_list = Set.of_list (module T)
+    let union_list = Set.union_list (module T)
     let of_vector = Set.of_vector (module T)
   end
 

sledge/src/llair/exp.mli

@@ -97,6 +97,7 @@ module Var : sig
     val empty : t
     val of_option : var option -> t
     val of_list : var list -> t
+    val union_list : t list -> t
     val of_vector : var vector -> t
   end
 

sledge/src/sledge.ml

@@ -68,6 +68,22 @@ let unmarshal file () =
     ~f:(fun ic -> (Marshal.from_channel ic : Llair.t))
     file
 
+let used_globals pgm preanalyze =
+  if preanalyze then
+    let summary_table =
+      Used_globals_executor.compute_summaries
+        { bound= 1
+        ; skip_throw= false
+        ; function_summaries= true
+        ; globals= `Declared Var.Set.empty }
+        pgm
+    in
+    `Per_function (Map.map summary_table ~f:Var.Set.union_list)
+  else
+    `Declared
+      (Vector.fold pgm.globals ~init:Var.Set.empty ~f:(fun acc g ->
+           Set.add acc g.var ))
+
 let analyze =
   let%map_open bound =
     flag "bound"
@@ -79,6 +95,9 @@ let analyze =
   and function_summaries =
     flag "function-summaries" no_arg
       ~doc:"use function summaries (in development)"
+  and preanalyze_globals =
+    flag "preanalyze-globals" no_arg
+      ~doc:"pre-analyze global variables used by each function"
   and exec =
     flag "domain"
       (optional_with_default Sh_executor.exec_pgm
@@ -92,7 +111,9 @@ let analyze =
          \"unit\" (unit domain)"
   in
   fun program () ->
-    exec {bound; skip_throw; function_summaries} (program ())
+    let pgm = program () in
+    let globals = used_globals pgm preanalyze_globals in
+    exec {bound; skip_throw; function_summaries; globals} pgm
 
 let analyze_cmd =
   let summary = "analyze LLAIR code" in

sledge/src/symbheap/state_domain.ml

@@ -74,15 +74,13 @@ type from_call = {areturn: Var.t option; subst: Var.Subst.t; frame: Sh.t}
 (** Express formula in terms of formals instead of actuals, and enter scope
     of locals: rename formals to fresh vars in formula and actuals, add
     equations between each formal and actual, and quantify fresh vars. *)
-let call ~summaries actuals areturn formals locals globals_vec q =
+let call ~summaries ~globals actuals areturn formals ~locals q =
   [%Trace.call fun {pf} ->
     pf
       "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ \
        globals: {@[%a@]}@ q: %a@]"
       (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
-      (List.rev formals) Var.Set.pp locals
-      (Vector.pp ",@ " Llair_.Global.pp)
-      globals_vec pp q]
+      (List.rev formals) Var.Set.pp locals Var.Set.pp globals pp q]
   ;
   let q', freshen_locals =
     Sh.freshen q ~wrt:(Set.add_list formals locals)
@@ -101,11 +99,7 @@ let call ~summaries actuals areturn formals locals globals_vec q =
   else
     (* Add the formals here to do garbage collection and then get rid of
        them *)
-    let formals_set = Var.Set.of_list formals
-    and globals =
-      Var.Set.of_vector
-        (Vector.map globals_vec ~f:(fun (g : Global.t) -> g.var))
-    in
+    let formals_set = Var.Set.of_list formals in
     let function_summary_pre =
       garbage_collect q'' ~wrt:(Set.union formals_set globals)
     in