[sledge] Add used-globals abstract domain and transfer functions

Summary:
Adds an abstract domain to track global variable usages, as well as supporting
changes to the frontend, IR and CLI.  This analysis will support optimizations
to the main symbolic-heap analysis, but for now can be invoked independently
through the `-domain` flag on `analyze` targets of the Sledge executable.

Reviewed By: jberdine

Differential Revision: D17422212

fbshipit-source-id: 74bed0a76

sledge/sledge-help.txt

@@ -47,6 +47,9 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s
 
   [-bound <int>]          stop execution exploration at depth <int>
   [-colors]               enable printing in colors
+  [-domain <string>]      select abstract domain; must be one of "sh" (default,
+                          symbolic heap domain), "globals" (used-globals
+                          domain), or "unit" (unit domain)
   [-function-summaries]   use function summaries (in development)
   [-fuzzer]               add a harness for libFuzzer targets
   [-llair-output <file>]  write generated LLAIR to <file>
@@ -55,8 +58,6 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s
                           output if <file> is `-`
   [-skip-throw]           do not explore past throwing an exception
   [-trace <spec>]         enable debug tracing
-  [-unit-domain]          use unit domain (experimental, debugging purposes
-                          only)
   [-help]                 print this help text and exit
                           (alias: -?)
 
@@ -128,14 +129,15 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo
 
   [-bound <int>]          stop execution exploration at depth <int>
   [-colors]               enable printing in colors
+  [-domain <string>]      select abstract domain; must be one of "sh" (default,
+                          symbolic heap domain), "globals" (used-globals
+                          domain), or "unit" (unit domain)
   [-function-summaries]   use function summaries (in development)
   [-fuzzer]               add a harness for libFuzzer targets
   [-llair-output <file>]  write generated LLAIR to <file>
   [-margin <cols>]        wrap debug tracing at <cols> columns
   [-skip-throw]           do not explore past throwing an exception
   [-trace <spec>]         enable debug tracing
-  [-unit-domain]          use unit domain (experimental, debugging purposes
-                          only)
   [-help]                 print this help text and exit
                           (alias: -?)
 
@@ -171,11 +173,13 @@ The <input> file must be binary LLAIR, such as produced by `sledge translate`.
 
   [-bound <int>]         stop execution exploration at depth <int>
   [-colors]              enable printing in colors
+  [-domain <string>]     select abstract domain; must be one of "sh" (default,
+                         symbolic heap domain), "globals" (used-globals domain),
+                         or "unit" (unit domain)
   [-function-summaries]  use function summaries (in development)
   [-margin <cols>]       wrap debug tracing at <cols> columns
   [-skip-throw]          do not explore past throwing an exception
   [-trace <spec>]        enable debug tracing
-  [-unit-domain]         use unit domain (experimental, debugging purposes only)
   [-help]                print this help text and exit
                          (alias: -?)
 

sledge/src/control.ml

@@ -443,7 +443,7 @@ module Make (Dom : Domain_sig.Dom) = struct
    fun opts pgm ->
     let entry_points = Config.find_list "entry-points" in
     List.find_map entry_points ~f:(fun name ->
-        Llair.Func.find pgm.functions (Var.program name) )
+        Llair.Func.find pgm.functions (Var.program ~global:() name) )
     |> function
     | Some {locals; params= []; entry} ->
         Some

sledge/src/domain/used_globals.ml

@@ -0,0 +1,68 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Used-globals abstract domain *)
+
+type t = Var.Set.t [@@deriving equal, sexp_of]
+
+let pp = Set.pp Var.pp
+let report_fmt_thunk = Fn.flip pp
+let empty = Var.Set.empty
+
+let init globals =
+  [%Trace.info
+    "pgm globals: {%a}" (Vector.pp ", " Llair_.Global.pp) globals] ;
+  empty
+
+let join = Set.union
+let is_false _ = false
+let post _ _ state = state
+let retn _ _ from_call post = Set.union from_call post
+let dnf t = [t]
+let add_if_global gs v = if Var.global v then Set.add gs v else gs
+
+let used_globals ?(init = empty) exp =
+  Exp.fold_vars exp ~init ~f:add_if_global
+
+let exec_assume st exp = Some (used_globals ~init:st exp)
+let exec_kill st _ = st
+let exec_move st _ rhs = used_globals ~init:st rhs
+
+let exec_inst st inst =
+  [%Trace.call fun {pf} -> pf "{%a} %a { ? }" pp st Llair.Inst.pp inst]
+  ;
+  Ok
+    (Llair.Inst.fold_exps inst ~init:st ~f:(fun acc e ->
+         used_globals ~init:acc e ))
+  |>
+  [%Trace.retn fun {pf} res ->
+    match res with
+    | Ok uses -> pf "new uses: %a" pp (Set.diff uses st)
+    | _ -> ()]
+
+let exec_intrinsic ~skip_throw:_ st _ _ actuals =
+  List.fold actuals ~init:st ~f:(fun s a -> used_globals ~init:s a)
+  |> fun res -> Some (Ok res)
+
+type from_call = t [@@deriving sexp_of]
+
+(* Set abstract state to bottom (i.e. empty set) at function entry *)
+let call ~summaries:_ actuals _ _ _ _ st =
+  (empty, List.fold actuals ~init:st ~f:(fun s a -> used_globals ~init:s a))
+
+let resolve_callee lookup ptr _ =
+  match Var.of_exp ptr with
+  | Some callee_name -> lookup callee_name
+  | None -> []
+
+(* A function summary is the set of global variables accessed by that
+   function and its transitive callees *)
+type summary = t
+
+let pp_summary = pp
+let create_summary ~locals:_ ~formals:_ state = (state, state)
+let apply_summary st summ = Some (Set.union st summ)

sledge/src/domain/used_globals.mli

@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Used-globals abstract domain *)
+
+include Domain_sig.Dom

sledge/src/llair/exp.ml

@@ -65,7 +65,7 @@ module rec T : sig
     | Memory of {siz: t; arr: t}
     | Concat of {args: t vector}
     (* nullary *)
-    | Var of {id: int; name: string}
+    | Var of {id: int; name: string; global: bool}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
     (* curried application *)
@@ -130,7 +130,7 @@ and T0 : sig
     | Splat of {byt: t; siz: t}
     | Memory of {siz: t; arr: t}
     | Concat of {args: t vector}
-    | Var of {id: int; name: string}
+    | Var of {id: int; name: string; global: bool}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
     | App of {op: t; arg: t}
@@ -174,7 +174,7 @@ end = struct
     | Splat of {byt: t; siz: t}
     | Memory of {siz: t; arr: t}
     | Concat of {args: t vector}
-    | Var of {id: int; name: string}
+    | Var of {id: int; name: string; global: bool}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
     | App of {op: t; arg: t}
@@ -254,9 +254,11 @@ let rec pp ?is_x fs exp =
       Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
     in
     match exp with
-    | Var {name; id= 0} as var ->
+    | Var {name; id= 0; global= true} as var ->
+        Trace.pp_styled (get_var_style var) "%@%s" fs name
+    | Var {name; id= 0; global= false} as var ->
         Trace.pp_styled (get_var_style var) "%%%s" fs name
-    | Var {name; id} as var ->
+    | Var {name; id; _} as var ->
         Trace.pp_styled (get_var_style var) "%%%s_%d" fs name id
     | Nondet {msg} -> pf "nondet \"%s\"" msg
     | Label {name} -> pf "%s" name
@@ -460,7 +462,10 @@ let invariant ?(partial = false) e =
         assert_arity 0 ;
         assert (Z.numbits data <= bits) )
   | Integer _ -> assert false
-  | Var _ | Nondet _ | Label _ | Float _ -> assert_arity 0
+  | Var {id; global; _} ->
+      assert_arity 0 ;
+      assert ((not global) || id = 0)
+  | Nondet _ | Label _ | Float _ -> assert_arity 0
   | Convert {dst; src} ->
       ( match args with
       | [Integer {typ= Integer _ as typ}] -> assert (Typ.equal src typ)
@@ -567,16 +572,18 @@ module Var = struct
 
   let id = function Var {id} -> id | x -> violates invariant x
   let name = function Var {name} -> name | x -> violates invariant x
+  let global = function Var {global} -> global | x -> violates invariant x
 
   let of_exp = function
     | Var _ as v -> Some (v |> check invariant)
     | _ -> None
 
-  let program name = Var {id= 0; name} |> check invariant
+  let program ?global name =
+    Var {id= 0; name; global= Option.is_some global} |> check invariant
 
   let fresh name ~(wrt : Set.t) =
     let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in
-    let x' = Var {name; id= max + 1} in
+    let x' = Var {name; id= max + 1; global= false} in
     (x', Set.add wrt x')
 
   (** Variable renaming substitutions *)

sledge/src/llair/exp.mli

@@ -27,7 +27,8 @@ and t = private
       (** Iterated concatenation of a single byte *)
   | Memory of {siz: t; arr: t}  (** Size-tagged byte-array *)
   | Concat of {args: t vector}  (** Byte-array concatenation *)
-  | Var of {id: int; name: string}  (** Local variable / virtual register *)
+  | Var of {id: int; name: string; global: bool}
+      (** Local variable / virtual register *)
   | Nondet of {msg: string}
       (** Anonymous local variable with arbitrary value, representing
           non-deterministic approximation of value described by [msg] *)
@@ -112,10 +113,11 @@ module Var : sig
   include Invariant.S with type t := t
 
   val of_exp : exp -> t option
-  val program : string -> t
+  val program : ?global:unit -> string -> t
   val fresh : string -> wrt:Set.t -> t * Set.t
   val id : t -> int
   val name : t -> string
+  val global : t -> bool
 
   module Subst : sig
     type t [@@deriving compare, equal, sexp]

sledge/src/llair/frontend.ml

@@ -288,8 +288,7 @@ let xlate_float : Llvm.llvalue -> Exp.t =
   let data = suffix_after_last_space (Llvm.string_of_llvalue llv) in
   Exp.float data
 
-let xlate_name : Llvm.llvalue -> Var.t =
- fun llv -> Var.program (find_name llv)
+let xlate_name ?global llv = Var.program ?global (find_name llv)
 
 let xlate_name_opt : Llvm.llvalue -> Var.t option =
  fun instr ->
@@ -358,7 +357,7 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t =
         let fname = Llvm.value_name func in
         match xlate_intrinsic_exp fname with
         | Some intrinsic when inline || should_inline llv -> intrinsic x llv
-        | _ -> Exp.var (xlate_name llv) )
+        | _ -> Exp.var (xlate_name ~global:() llv) )
     | Instruction (Invoke | Alloca | Load | PHI | LandingPad | VAArg)
      |Argument ->
         Exp.var (xlate_name llv)
@@ -604,7 +603,7 @@ and xlate_global : x -> Llvm.llvalue -> Global.t =
   Hashtbl.find_or_add memo_global llg ~default:(fun () ->
       [%Trace.call fun {pf} -> pf "%a" pp_llvalue llg]
       ;
-      let g = xlate_name llg in
+      let g = xlate_name ~global:() llg in
       let llt = Llvm.type_of llg in
       let typ = xlate_type x llt in
       let loc = find_loc llg in
@@ -754,7 +753,7 @@ let pp_code fs (insts, term, blocks) =
 
 let rec xlate_func_name x llv =
   match Llvm.classify_value llv with
-  | Function -> Exp.var (xlate_name llv)
+  | Function -> Exp.var (xlate_name ~global:() llv)
   | ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv)
   | Argument | Instruction _ -> xlate_value x llv
   | GlobalAlias -> xlate_func_name x (Llvm.operand llv 0)

sledge/src/llair/global.ml

@@ -26,7 +26,8 @@ let pp_defn fs {var; init; typ; loc} =
 let invariant g =
   Invariant.invariant [%here] g [%sexp_of: t]
   @@ fun () ->
-  let {typ} = g in
-  assert (Typ.is_sized typ)
+  let {var; typ} = g in
+  assert (Typ.is_sized typ) ;
+  assert (Var.global var)
 
 let mk ?init var typ loc = {var; init; typ; loc} |> check invariant

sledge/src/llair/llair.ml

@@ -219,7 +219,7 @@ let rec dummy_block =
   ; sort_index= 0 }
 
 and dummy_func =
-  let dummy_var = Var.program "dummy" in
+  let dummy_var = Var.program ~global:() "dummy" in
   let dummy_ptr_typ = Typ.pointer ~elt:(Typ.opaque ~name:"dummy") in
   { name= Global.mk dummy_var dummy_ptr_typ Loc.none
   ; params= []
@@ -271,6 +271,20 @@ module Inst = struct
         vs
 
   let locals inst = union_locals inst Var.Set.empty
+
+  let fold_exps inst ~init ~f =
+    match inst with
+    | Move {reg_exps; loc= _} ->
+        Vector.fold reg_exps ~init ~f:(fun acc (_reg, exp) -> f acc exp)
+    | Load {reg= _; ptr; len; loc= _} -> f (f init ptr) len
+    | Store {ptr; exp; len; loc= _} -> f (f (f init ptr) exp) len
+    | Memset {dst; byt; len; loc= _} -> f (f (f init dst) byt) len
+    | Memcpy {dst; src; len; loc= _} | Memmov {dst; src; len; loc= _} ->
+        f (f (f init dst) src) len
+    | Alloc {reg= _; num; len; loc= _} -> f (f init num) len
+    | Free {ptr; loc= _} -> f init ptr
+    | Nondet {reg= _; msg= _; loc= _} -> init
+    | Abort {loc= _} -> init
 end
 
 (** Jumps *)

sledge/src/llair/llair.mli

@@ -124,6 +124,7 @@ module Inst : sig
   val abort : loc:Loc.t -> inst
   val loc : inst -> Loc.t
   val locals : inst -> Var.Set.t
+  val fold_exps : inst -> init:'a -> f:('a -> Exp.t -> 'a) -> 'a
 end
 
 module Jump : sig

sledge/src/sledge.ml

@@ -15,6 +15,7 @@ type 'a param = 'a Command.Param.t
 
 module Sh_executor = Control.Make (Domain.Relation.Make (State_domain))
 module Unit_executor = Control.Make (Domain.Unit)
+module Used_globals_executor = Control.Make (Domain.Used_globals)
 
 (* reverse application in the Command.Param applicative *)
 let ( |*> ) : 'a param -> ('a -> 'b) param -> 'b param =
@@ -78,12 +79,17 @@ let analyze =
   and function_summaries =
     flag "function-summaries" no_arg
       ~doc:"use function summaries (in development)"
-  and unit_domain =
-    flag "unit-domain" no_arg
-      ~doc:"use unit domain (experimental, debugging purposes only)"
-  in
-  let exec =
-    if unit_domain then Unit_executor.exec_pgm else Sh_executor.exec_pgm
+  and exec =
+    flag "domain"
+      (optional_with_default Sh_executor.exec_pgm
+         (Arg_type.of_alist_exn
+            [ ("sh", Sh_executor.exec_pgm)
+            ; ("globals", Used_globals_executor.exec_pgm)
+            ; ("unit", Unit_executor.exec_pgm) ]))
+      ~doc:
+        "<string> select abstract domain; must be one of \"sh\" (default, \
+         symbolic heap domain), \"globals\" (used-globals domain), or \
+         \"unit\" (unit domain)"
   in
   fun program () ->
     exec {bound; skip_throw; function_summaries} (program ())

sledge/src/symbheap/state_domain.ml

@@ -77,9 +77,12 @@ type from_call = {areturn: Var.t option; subst: Var.Subst.t; frame: Sh.t}
 let call ~summaries actuals areturn formals locals globals_vec q =
   [%Trace.call fun {pf} ->
     pf
-      "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ q: %a@]"
+      "@[<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 pp q]
+      (List.rev formals) Var.Set.pp locals
+      (Vector.pp ",@ " Llair_.Global.pp)
+      globals_vec pp q]
   ;
   let q', freshen_locals =
     Sh.freshen q ~wrt:(Set.add_list formals locals)