From 47f314c00e7ad04c08334f0182a44f9dc1e71696 Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Wed, 18 Sep 2019 08:38:32 -0700 Subject: [PATCH] [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 | 14 +++--- sledge/src/control.ml | 2 +- sledge/src/domain/used_globals.ml | 68 +++++++++++++++++++++++++++++ sledge/src/domain/used_globals.mli | 10 +++++ sledge/src/llair/exp.ml | 23 ++++++---- sledge/src/llair/exp.mli | 6 ++- sledge/src/llair/frontend.ml | 9 ++-- sledge/src/llair/global.ml | 5 ++- sledge/src/llair/llair.ml | 16 ++++++- sledge/src/llair/llair.mli | 1 + sledge/src/sledge.ml | 18 +++++--- sledge/src/symbheap/state_domain.ml | 7 ++- 12 files changed, 147 insertions(+), 32 deletions(-) create mode 100644 sledge/src/domain/used_globals.ml create mode 100644 sledge/src/domain/used_globals.mli diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt index 4e82a9ae9..5eab72cf4 100644 --- a/sledge/sledge-help.txt +++ b/sledge/sledge-help.txt @@ -47,6 +47,9 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s [-bound ] stop execution exploration at depth [-colors] enable printing in colors + [-domain ] 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 ] write generated LLAIR to @@ -55,8 +58,6 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s output if is `-` [-skip-throw] do not explore past throwing an exception [-trace ] 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 ] stop execution exploration at depth [-colors] enable printing in colors + [-domain ] 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 ] write generated LLAIR to [-margin ] wrap debug tracing at columns [-skip-throw] do not explore past throwing an exception [-trace ] 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 file must be binary LLAIR, such as produced by `sledge translate`. [-bound ] stop execution exploration at depth [-colors] enable printing in colors + [-domain ] 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 ] wrap debug tracing at columns [-skip-throw] do not explore past throwing an exception [-trace ] enable debug tracing - [-unit-domain] use unit domain (experimental, debugging purposes only) [-help] print this help text and exit (alias: -?) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 21de31b48..2347f9a17 100644 --- a/sledge/src/control.ml +++ b/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 diff --git a/sledge/src/domain/used_globals.ml b/sledge/src/domain/used_globals.ml new file mode 100644 index 000000000..cbd7813d2 --- /dev/null +++ b/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) diff --git a/sledge/src/domain/used_globals.mli b/sledge/src/domain/used_globals.mli new file mode 100644 index 000000000..bf5b74ca9 --- /dev/null +++ b/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 diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 08b3d58eb..4c49e811f 100644 --- a/sledge/src/llair/exp.ml +++ b/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 *) diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index 63ccdbaf2..7b76d1b4b 100644 --- a/sledge/src/llair/exp.mli +++ b/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] diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index e1983af3c..3b3daa9b8 100644 --- a/sledge/src/llair/frontend.ml +++ b/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) diff --git a/sledge/src/llair/global.ml b/sledge/src/llair/global.ml index fbcaf2f28..4397be474 100644 --- a/sledge/src/llair/global.ml +++ b/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 diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index a82cbaafa..ab1b040a7 100644 --- a/sledge/src/llair/llair.ml +++ b/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 *) diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index e3c17b696..cd02fce51 100644 --- a/sledge/src/llair/llair.mli +++ b/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 diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml index 849df1036..7888f957e 100644 --- a/sledge/src/sledge.ml +++ b/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: + " 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 ()) diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml index b5d5e9b91..17063e307 100644 --- a/sledge/src/symbheap/state_domain.ml +++ b/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 - "@[actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ q: %a@]" + "@[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)