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