From 1e4e650dec9994420a7891fdee1c71fb8ee63847 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 2 Dec 2020 13:50:09 -0800 Subject: [PATCH] [sledge] Change execution options from a record to a module Summary: Currently the symbolic execution options, obtained from the command line flags and preanalysis, are passed to the Control entry points as a record, and then passed around within Control as needed. This diff simplifies the code in Control by replacing the record mechanism with an additional functor parameter containing the options. The main benefit is that the bound option no longer needs to be part of the analysis state. This change does make the code in Sledge_cli slightly more complicated, as it now performs a functor application using a first-class module computed from the command line flags. Reviewed By: jvillard Differential Revision: D25196735 fbshipit-source-id: 80e5d5d62 --- sledge/cli/sledge_cli.ml | 56 +++++++------ sledge/src/control.ml | 121 ++++++++++++----------------- sledge/src/control.mli | 12 +-- sledge/src/domain_intf.ml | 18 +++++ sledge/src/domain_used_globals.ml | 6 +- sledge/src/domain_used_globals.mli | 7 +- 6 files changed, 106 insertions(+), 114 deletions(-) diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml index 789d1b819..c4585f20e 100644 --- a/sledge/cli/sledge_cli.ml +++ b/sledge/cli/sledge_cli.ml @@ -12,11 +12,6 @@ open Command.Let_syntax type 'a param = 'a Command.Param.t -module Sh_executor = Control.Make (Domain_relation.Make (Domain_sh)) -module Unit_executor = Control.Make (Domain_unit) -module Used_globals_executor = Control.Make (Domain_used_globals) -module Itv_executor = Control.Make (Domain_itv) - (* reverse application in the Command.Param applicative *) let ( |*> ) : 'a param -> ('a -> 'b) param -> 'b param = fun x f -> x |> Command.Param.apply f @@ -78,16 +73,16 @@ let unmarshal file () = let entry_points = Config.find_list "entry-points" -let used_globals pgm preanalyze : Domain_used_globals.r = +let used_globals pgm entry_points preanalyze : Domain_intf.used_globals = if preanalyze then - let summary_table = - Used_globals_executor.compute_summaries - { bound= 1 - ; function_summaries= true - ; entry_points - ; globals= Declared Llair.Global.Set.empty } - pgm - in + let module Opts = struct + let bound = 1 + let function_summaries = true + let entry_points = entry_points + let globals = Domain_intf.Declared Llair.Global.Set.empty + end in + let module Analysis = Control.Make (Opts) (Domain_used_globals) in + let summary_table = Analysis.compute_summaries pgm in Per_function (Llair.Function.Map.map summary_table ~f:Llair.Global.Set.union_list) else @@ -106,14 +101,14 @@ let analyze = and preanalyze_globals = flag "preanalyze-globals" no_arg ~doc:"pre-analyze global variables used by each function" - and exec = + and domain = flag "domain" - (optional_with_default Sh_executor.exec_pgm + (optional_with_default `sh (Arg_type.of_alist_exn - [ ("sh", Sh_executor.exec_pgm) - ; ("globals", Used_globals_executor.exec_pgm) - ; ("unit", Unit_executor.exec_pgm) - ; ("itv", Itv_executor.exec_pgm) ])) + [ ("sh", `sh) + ; ("globals", `globals) + ; ("itv", `itv) + ; ("unit", `unit) ])) ~doc: " select abstract domain; must be one of \"sh\" (default, \ symbolic heap domain), \"globals\" (used-globals domain), or \ @@ -125,11 +120,26 @@ let analyze = flag "stats" no_arg ~doc:"output performance statistics to stderr" in fun program () -> + Timer.enabled := stats ; let pgm = program () in - let globals = used_globals pgm preanalyze_globals in + let globals = used_globals pgm entry_points preanalyze_globals in + let module Opts = struct + let bound = bound + let function_summaries = function_summaries + let entry_points = entry_points + let globals = globals + end in + let dom : (module Domain_intf.Dom) = + match domain with + | `sh -> (module Domain_relation.Make (Domain_sh)) + | `globals -> (module Domain_used_globals) + | `itv -> (module Domain_itv) + | `unit -> (module Domain_unit) + in + let module Dom = (val dom) in + let module Analysis = Control.Make (Opts) (Dom) in Domain_sh.simplify_states := not no_simplify_states ; - Timer.enabled := stats ; - exec {bound; function_summaries; entry_points; globals} pgm ; + Analysis.exec_pgm pgm ; Report.coverage pgm ; Report.safe_or_unsafe () diff --git a/sledge/src/control.ml b/sledge/src/control.ml index a1508d492..da2aa01ba 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -9,13 +9,7 @@ The analysis' semantics of control flow. *) -type exec_opts = - { bound: int - ; function_summaries: bool - ; entry_points: string list - ; globals: Domain_used_globals.r } - -module Make (Dom : Domain_intf.Dom) = struct +module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct module Stack : sig type t @@ -24,10 +18,7 @@ module Make (Dom : Domain_intf.Dom) = struct type as_inlined_location = t [@@deriving compare, sexp_of] val empty : t - - val push_call : - Llair.func Llair.call -> bound:int -> Dom.from_call -> t -> t option - + val push_call : Llair.func Llair.call -> Dom.from_call -> t -> t option val pop_return : t -> (Dom.from_call * Llair.jump * t) option val pop_throw : @@ -107,7 +98,7 @@ module Make (Dom : Domain_intf.Dom) = struct (match jmp with None -> stk | Some jmp -> Throw (jmp, stk)) |> check invariant - let push_call (Llair.{return; throw} as call) ~bound from_call stk = + let push_call (Llair.{return; throw} as call) from_call stk = [%Trace.call fun {pf} -> pf "%a" pp stk] ; let rec count_f_in_stack acc f = function @@ -118,7 +109,7 @@ module Make (Dom : Domain_intf.Dom) = struct | _ -> acc in let n = count_f_in_stack 0 return stk in - ( if n > bound then ( + ( if n > Opts.bound then ( Report.hit_bound n ; None ) else Some (push_throw throw (push_return call from_call stk)) ) @@ -146,7 +137,7 @@ module Make (Dom : Domain_intf.Dom) = struct module Work : sig type t - val init : Dom.t -> Llair.block -> int -> t + val init : Dom.t -> Llair.block -> t type x @@ -264,32 +255,32 @@ module Make (Dom : Domain_intf.Dom) = struct Some (top, elts, {queue; removed}) end - type t = PrioQueue.t * int + type t = PrioQueue.t 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 (queue, bound) = + let add ?prev ~retreating stk state curr depths queue = 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 <= Opts.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) ) + PrioQueue.add {depth; edge; state; depths} queue ) else ( [%Trace.info "prune: %i: %a" depth Edge.pp edge] ; - Report.hit_bound bound ; - (queue, bound) ) + Report.hit_bound Opts.bound ; + queue ) - let init state curr bound = + let init state curr = add ~retreating:false Stack.empty state curr Depths.empty - (PrioQueue.create (), bound) + (PrioQueue.create ()) - let rec run ~f (queue, bound) = + let rec run ~f queue = match PrioQueue.pop queue with | Some ({depth; edge; state; depths}, elts, queue) -> [%Trace.info @@ -305,7 +296,7 @@ module Make (Dom : Domain_intf.Dom) = struct (state, depths, queue) | None -> (state, depths, queue) ) in - run ~f (f edge.stk state edge.dst depths (queue, bound)) + run ~f (f edge.stk state edge.dst depths queue) | None -> [%Trace.info "queue empty"] ; () @@ -316,7 +307,7 @@ module Make (Dom : Domain_intf.Dom) = struct let summary_table = Llair.Function.Tbl.create () - let exec_call opts stk state block call globals = + let exec_call stk state block call globals = let Llair.{callee; actuals; areturn; return; recursive} = call in let Llair.{name; formals; freturn; locals; entry} = callee in [%Trace.call fun {pf} -> @@ -324,14 +315,14 @@ module Make (Dom : Domain_intf.Dom) = struct Llair.Function.pp return.dst.parent.name Dom.pp state] ; let dnf_states = - if opts.function_summaries then Dom.dnf state else [state] + if Opts.function_summaries then Dom.dnf state else [state] in let domain_call = Dom.call ~globals ~actuals ~areturn ~formals ~freturn ~locals in List.fold dnf_states Work.skip ~f:(fun state acc -> match - if not opts.function_summaries then None + if not Opts.function_summaries then None else let maybe_summary_post = let state = fst (domain_call ~summaries:false state) in @@ -345,12 +336,10 @@ module Make (Dom : Domain_intf.Dom) = struct with | None -> let state, from_call = - domain_call ~summaries:opts.function_summaries state + domain_call ~summaries:Opts.function_summaries state in Work.seq acc - ( match - Stack.push_call call ~bound:opts.bound from_call stk - with + ( match Stack.push_call call from_call stk with | Some stk -> Work.add stk ~prev:block ~retreating:recursive state entry | None -> ( @@ -373,11 +362,11 @@ module Make (Dom : Domain_intf.Dom) = struct let state = Option.fold ~f:Dom.exec_kill areturn state in exec_jump stk state block return - let exec_call opts stk state block - ({Llair.callee; areturn; return; _} as call) globals = + let exec_call stk state block ({Llair.callee; areturn; return; _} as call) + globals = if Llair.Func.is_undefined callee then exec_skip_func stk state block areturn return - else exec_call opts stk state block call globals + else exec_call stk state block call globals let pp_st () = [%Trace.printf @@ -387,12 +376,12 @@ module Make (Dom : Domain_intf.Dom) = struct (List.pp "@," Dom.pp_summary) data ) )] - let exec_return ~opts stk pre_state (block : Llair.block) exp = + let exec_return stk pre_state (block : Llair.block) exp = let Llair.{name; formals; freturn; locals} = block.parent in [%Trace.call fun {pf} -> pf "from: %a" Llair.Function.pp name] ; let summarize post_state = - if not opts.function_summaries then post_state + if not Opts.function_summaries then post_state else let function_summary, post_state = Dom.create_summary ~locals ~formals post_state @@ -417,10 +406,10 @@ module Make (Dom : Domain_intf.Dom) = struct | None -> (* Create and store a function summary for main *) if - opts.function_summaries + Opts.function_summaries && List.mem ~eq:String.equal (Llair.Function.name name) - opts.entry_points + Opts.entry_points then summarize exit_state |> (ignore : Dom.t -> unit) ; Work.skip ) |> @@ -449,14 +438,9 @@ module Make (Dom : Domain_intf.Dom) = struct |> [%Trace.retn fun {pf} _ -> pf ""] - let exec_term : - exec_opts - -> Llair.program - -> Stack.t - -> Dom.t - -> Llair.block - -> Work.x = - fun opts pgm stk state block -> + let exec_term : Llair.program -> Stack.t -> Dom.t -> Llair.block -> Work.x + = + fun pgm stk state block -> [%Trace.info "@[<2>exec term@\n@[%a@]@\n%a@]" Dom.pp state Llair.Term.pp block.term] ; Report.step_term block.term ; @@ -487,18 +471,18 @@ module Make (Dom : Domain_intf.Dom) = struct | Some state -> exec_jump stk state block jump |> Work.seq x | None -> x ) | Call ({callee} as call) -> - exec_call opts stk state block call - (Domain_used_globals.by_function opts.globals callee.name) + exec_call stk state block call + (Domain_used_globals.by_function Opts.globals callee.name) | ICall ({callee; areturn; return} as call) -> ( let lookup name = Llair.Func.find name pgm.functions in match Dom.resolve_callee lookup callee state with | [] -> exec_skip_func stk state block areturn return | callees -> List.fold callees Work.skip ~f:(fun callee x -> - exec_call opts stk state block {call with callee} - (Domain_used_globals.by_function opts.globals callee.name) + exec_call stk state block {call with callee} + (Domain_used_globals.by_function Opts.globals callee.name) |> Work.seq x ) ) - | Return {exp} -> exec_return ~opts stk state block exp + | Return {exp} -> exec_return stk state block exp | Throw {exc} -> exec_throw stk state block exc | Unreachable -> Work.skip @@ -513,13 +497,8 @@ module Make (Dom : Domain_intf.Dom) = struct | Some state -> Result.Ok state | None -> Result.Error (state, inst) let exec_block : - exec_opts - -> Llair.program - -> Stack.t - -> Dom.t - -> Llair.block - -> Work.x = - fun opts pgm stk state block -> + Llair.program -> Stack.t -> Dom.t -> Llair.block -> Work.x = + fun pgm stk state block -> [%trace] ~call:(fun {pf} -> pf "#%i %%%s in %a" block.sort_index block.lbl Llair.Function.pp @@ -531,39 +510,39 @@ module Make (Dom : Domain_intf.Dom) = struct match Iter.fold_result ~f:exec_inst (IArray.to_iter block.cmnd) state with - | Ok state -> exec_term opts pgm stk state block + | Ok state -> exec_term pgm stk state block | Error (state, inst) -> Report.invalid_access_inst (Dom.report_fmt_thunk state) inst ; Work.skip - let harness : exec_opts -> Llair.program -> (int -> Work.t) option = - fun opts pgm -> + let harness : Llair.program -> Work.t option = + fun pgm -> List.find_map ~f:(fun entry_point -> Llair.Func.find entry_point pgm.functions) - opts.entry_points + Opts.entry_points |> function | Some {name; formals; freturn; locals; entry} when IArray.is_empty formals -> Some (Work.init (fst - (Dom.call ~summaries:opts.function_summaries + (Dom.call ~summaries:Opts.function_summaries ~globals: - (Domain_used_globals.by_function opts.globals name) + (Domain_used_globals.by_function Opts.globals name) ~actuals:IArray.empty ~areturn:None ~formals:IArray.empty ~freturn ~locals (Dom.init pgm.globals))) entry) | _ -> None - let exec_pgm : exec_opts -> Llair.program -> unit = - fun opts pgm -> - match harness opts pgm with - | Some work -> Work.run ~f:(exec_block opts pgm) (work opts.bound) + let exec_pgm : Llair.program -> unit = + fun pgm -> + match harness pgm with + | Some work -> Work.run ~f:(exec_block pgm) work | None -> fail "no applicable harness" () - let compute_summaries opts pgm : Dom.summary list Llair.Function.Map.t = - assert opts.function_summaries ; - exec_pgm opts pgm ; + let compute_summaries pgm : Dom.summary list Llair.Function.Map.t = + assert Opts.function_summaries ; + exec_pgm pgm ; Llair.Function.Tbl.fold summary_table Llair.Function.Map.empty ~f:(fun ~key ~data map -> match data with diff --git a/sledge/src/control.mli b/sledge/src/control.mli index cf8619fd1..17b5070fc 100644 --- a/sledge/src/control.mli +++ b/sledge/src/control.mli @@ -7,15 +7,9 @@ (** The analysis' semantics of control flow. *) -type exec_opts = - { bound: int (** Loop/recursion unrolling bound *) - ; function_summaries: bool (** Use function summarisation *) - ; entry_points: string list (** C linkage names of entry points *) - ; globals: Domain_used_globals.r } - -module Make (Dom : Domain_intf.Dom) : sig - val exec_pgm : exec_opts -> Llair.program -> unit +module Make (_ : Domain_intf.Opts) (Dom : Domain_intf.Dom) : sig + val exec_pgm : Llair.program -> unit val compute_summaries : - exec_opts -> Llair.program -> Dom.summary list Llair.Function.Map.t + Llair.program -> Dom.summary list Llair.Function.Map.t end diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml index 6a79c8a6b..de84026e1 100644 --- a/sledge/src/domain_intf.ml +++ b/sledge/src/domain_intf.ml @@ -50,3 +50,21 @@ module type Dom = sig val apply_summary : t -> summary -> t option end + +type used_globals = + | Per_function of Llair.Global.Set.t Llair.Function.Map.t + (** per-function used-globals map *) + | Declared of Llair.Global.Set.t (** program-wide set *) + +module type Opts = sig + val bound : int + (** Loop/recursion unrolling bound *) + + val function_summaries : bool + (** Use function summarization *) + + val entry_points : string list + (** C linkage names of entry points *) + + val globals : used_globals +end diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml index ceb23cec0..9f2ced8d1 100644 --- a/sledge/src/domain_used_globals.ml +++ b/sledge/src/domain_used_globals.ml @@ -64,11 +64,7 @@ let apply_summary st summ = Some (Llair.Global.Set.union st summ) (** Query *) -type r = - | Per_function of Llair.Global.Set.t Llair.Function.Map.t - | Declared of Llair.Global.Set.t - -let by_function : r -> Llair.Function.t -> t = +let by_function : Domain_intf.used_globals -> Llair.Function.t -> t = fun s fn -> [%Trace.call fun {pf} -> pf "%a" Llair.Function.pp fn] ; diff --git a/sledge/src/domain_used_globals.mli b/sledge/src/domain_used_globals.mli index c1a93a02e..ace20ab8e 100644 --- a/sledge/src/domain_used_globals.mli +++ b/sledge/src/domain_used_globals.mli @@ -9,9 +9,4 @@ include Domain_intf.Dom with type summary = Llair.Global.Set.t -type r = - | Per_function of Llair.Global.Set.t Llair.Function.Map.t - (** per-function used-globals map *) - | Declared of Llair.Global.Set.t (** program-wide set *) - -val by_function : r -> Llair.Function.t -> summary +val by_function : Domain_intf.used_globals -> Llair.Function.t -> summary