From 2acb1c3deec9bd712bd9c335d8bec7adfa53fdfa Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Thu, 12 Sep 2019 06:06:41 -0700 Subject: [PATCH] [sledge] Functorize worklist, separate out domain-specific logic Summary: Add support for future development of new abstract domains by eliminating hard-wired dependencies from the worklist into the symbolic heap domain. Also includes an implementation of a trivial unit domain and a CLI flag to enable its use, for debugging purposes. Reviewed By: jberdine Differential Revision: D17281681 fbshipit-source-id: 5858fd420 --- sledge/sledge-help.txt | 5 + sledge/src/control.ml | 870 +++++++++--------- sledge/src/control.mli | 4 +- sledge/src/domain_sig.ml | 57 ++ sledge/src/report.ml | 13 +- sledge/src/report.mli | 4 +- sledge/src/sledge.ml | 11 +- .../src/symbheap/{domain.ml => sh_domain.ml} | 6 +- .../symbheap/{domain.mli => sh_domain.mli} | 12 +- sledge/src/symbheap/state_domain.ml | 8 +- sledge/src/symbheap/state_domain.mli | 8 +- sledge/src/unit_domain.ml | 39 + sledge/src/unit_domain.mli | 10 + 13 files changed, 590 insertions(+), 457 deletions(-) create mode 100644 sledge/src/domain_sig.ml rename sledge/src/symbheap/{domain.ml => sh_domain.ml} (95%) rename sledge/src/symbheap/{domain.mli => sh_domain.mli} (85%) create mode 100644 sledge/src/unit_domain.ml create mode 100644 sledge/src/unit_domain.mli diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt index 556263afc..4e82a9ae9 100644 --- a/sledge/sledge-help.txt +++ b/sledge/sledge-help.txt @@ -55,6 +55,8 @@ 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: -?) @@ -132,6 +134,8 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo [-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,6 +175,7 @@ The file must be binary LLAIR, such as produced by `sledge translate`. [-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 b3dadf0d1..21de31b48 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -11,448 +11,456 @@ type exec_opts = {bound: int; skip_throw: bool; function_summaries: bool} -module Stack : sig - type t - type as_inlined_location = t [@@deriving compare, sexp_of] - - val empty : t - - val push_call : - Llair.func Llair.call -> bound:int -> Domain.from_call -> t -> t option - - val pop_return : t -> (Domain.from_call * Llair.jump * t) option - - val pop_throw : - t - -> init:'a - -> unwind:(Var.t list -> Var.Set.t -> Domain.from_call -> 'a -> 'a) - -> (Domain.from_call * Llair.jump * t * 'a) option -end = struct - type t = - | Return of - { recursive: bool (** return from a possibly-recursive call *) - ; dst: Llair.Jump.t - ; params: Var.t list - ; locals: Var.Set.t - ; from_call: Domain.from_call - ; stk: t } - | Throw of Llair.Jump.t * t - | Empty - [@@deriving sexp_of] - - type as_inlined_location = t [@@deriving sexp_of] - - (* Treat a stack as a code location in a hypothetical expansion of the - program where all non-recursive functions have been completely inlined. - In particular, this means to compare stacks as if all Return frames for - recursive calls had been removed. Additionally, the from_call info in - Return frames is ignored. *) - let rec compare_as_inlined_location x y = - if x == y then 0 - else - match (x, y) with - | Return {recursive= true; stk= x}, y - |x, Return {recursive= true; stk= y} -> - compare_as_inlined_location x y - | Return {dst= j; stk= x}, Return {dst= k; stk= y} -> ( - match Llair.Jump.compare j k with - | 0 -> compare_as_inlined_location x y - | n -> n ) - | Return _, _ -> -1 - | _, Return _ -> 1 - | Throw (j, x), Throw (k, y) -> ( - match Llair.Jump.compare j k with - | 0 -> compare_as_inlined_location x y - | n -> n ) - | Throw _, _ -> -1 - | _, Throw _ -> 1 - | Empty, Empty -> 0 - - let rec print_abbrev fs = function - | Return {recursive= false; stk= s} -> - print_abbrev fs s ; - Format.pp_print_char fs 'R' - | Return {recursive= true; stk= s} -> - print_abbrev fs s ; - Format.pp_print_string fs "R↑" - | Throw (_, s) -> - print_abbrev fs s ; - Format.pp_print_char fs 'T' - | Empty -> () - - let invariant s = - Invariant.invariant [%here] s [%sexp_of: t] - @@ fun () -> - match s with - | Return _ | Throw (_, Return _) | Empty -> () - | Throw _ -> fail "malformed stack: %a" print_abbrev s () - - let empty = Empty |> check invariant - - let push_return Llair.{callee= {params; locals}; return; recursive} - from_call stk = - Return {recursive; dst= return; params; locals; from_call; stk} - |> check invariant - - let push_throw jmp stk = - (match jmp with None -> stk | Some jmp -> Throw (jmp, stk)) - |> check invariant - - let push_call (Llair.{return; throw} as call) ~bound from_call stk = - [%Trace.call fun {pf} -> pf "%a" print_abbrev stk] - ; - let rec count_f_in_stack acc f = function - | Return {stk= next_frame; dst= dest_block} -> - count_f_in_stack - (if Llair.Jump.equal dest_block f then acc + 1 else acc) - f next_frame - | _ -> acc - in - let n = count_f_in_stack 0 return stk in - ( if n > bound then None - else Some (push_throw throw (push_return call from_call stk)) ) - |> - [%Trace.retn fun {pf} _ -> - pf "%d of %a on stack" n Llair.Jump.pp return] - - let rec pop_return = function - | Throw (_, stk) -> pop_return stk - | Return {from_call; dst; stk} -> Some (from_call, dst, stk) - | Empty -> None - - let pop_throw stk ~init ~unwind = - let rec pop_throw_ state = function - | Return {params; locals; from_call; stk} -> - pop_throw_ (unwind params locals from_call state) stk - | Throw (dst, Return {from_call; stk}) -> - Some (from_call, dst, stk, state) +module Make (Dom : Domain_sig.Dom) = struct + module Stack : sig + type t + 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 pop_return : t -> (Dom.from_call * Llair.jump * t) option + + val pop_throw : + t + -> init:'a + -> unwind:(Var.t list -> Var.Set.t -> Dom.from_call -> 'a -> 'a) + -> (Dom.from_call * Llair.jump * t * 'a) option + end = struct + type t = + | Return of + { recursive: bool (** return from a possibly-recursive call *) + ; dst: Llair.Jump.t + ; params: Var.t list + ; locals: Var.Set.t + ; from_call: Dom.from_call + ; stk: t } + | Throw of Llair.Jump.t * t + | Empty + [@@deriving sexp_of] + + type as_inlined_location = t [@@deriving sexp_of] + + (* Treat a stack as a code location in a hypothetical expansion of the + program where all non-recursive functions have been completely + inlined. In particular, this means to compare stacks as if all Return + frames for recursive calls had been removed. Additionally, the + from_call info in Return frames is ignored. *) + let rec compare_as_inlined_location x y = + if x == y then 0 + else + match (x, y) with + | Return {recursive= true; stk= x}, y + |x, Return {recursive= true; stk= y} -> + compare_as_inlined_location x y + | Return {dst= j; stk= x}, Return {dst= k; stk= y} -> ( + match Llair.Jump.compare j k with + | 0 -> compare_as_inlined_location x y + | n -> n ) + | Return _, _ -> -1 + | _, Return _ -> 1 + | Throw (j, x), Throw (k, y) -> ( + match Llair.Jump.compare j k with + | 0 -> compare_as_inlined_location x y + | n -> n ) + | Throw _, _ -> -1 + | _, Throw _ -> 1 + | Empty, Empty -> 0 + + let rec print_abbrev fs = function + | Return {recursive= false; stk= s} -> + print_abbrev fs s ; + Format.pp_print_char fs 'R' + | Return {recursive= true; stk= s} -> + print_abbrev fs s ; + Format.pp_print_string fs "R↑" + | Throw (_, s) -> + print_abbrev fs s ; + Format.pp_print_char fs 'T' + | Empty -> () + + let invariant s = + Invariant.invariant [%here] s [%sexp_of: t] + @@ fun () -> + match s with + | Return _ | Throw (_, Return _) | Empty -> () + | Throw _ -> fail "malformed stack: %a" print_abbrev s () + + let empty = Empty |> check invariant + + let push_return Llair.{callee= {params; locals}; return; recursive} + from_call stk = + Return {recursive; dst= return; params; locals; from_call; stk} + |> check invariant + + let push_throw jmp stk = + (match jmp with None -> stk | Some jmp -> Throw (jmp, stk)) + |> check invariant + + let push_call (Llair.{return; throw} as call) ~bound from_call stk = + [%Trace.call fun {pf} -> pf "%a" print_abbrev stk] + ; + let rec count_f_in_stack acc f = function + | Return {stk= next_frame; dst= dest_block} -> + count_f_in_stack + (if Llair.Jump.equal dest_block f then acc + 1 else acc) + f next_frame + | _ -> acc + in + let n = count_f_in_stack 0 return stk in + ( if n > bound then None + else Some (push_throw throw (push_return call from_call stk)) ) + |> + [%Trace.retn fun {pf} _ -> + pf "%d of %a on stack" n Llair.Jump.pp return] + + let rec pop_return = function + | Throw (_, stk) -> pop_return stk + | Return {from_call; dst; stk} -> Some (from_call, dst, stk) | Empty -> None - | Throw _ as stk -> violates invariant stk - in - pop_throw_ init stk -end -module Work : sig - type t - - val init : Domain.t -> Llair.block -> int -> t - - type x - - val skip : x - val seq : x -> x -> x - - val add : - ?prev:Llair.block - -> retreating:bool - -> Stack.t - -> Domain.t - -> Llair.block - -> x - - val run : f:(Stack.t -> Domain.t -> Llair.block -> x) -> t -> unit -end = struct - module Edge = struct - module T = struct - type t = - { dst: Llair.Block.t - ; src: Llair.Block.t option - ; stk: Stack.as_inlined_location } - [@@deriving compare, sexp_of] - end - - include T - include Comparator.Make (T) - - let pp fs {dst; src} = - Format.fprintf fs "#%i %s <--%a" dst.sort_index dst.lbl - (Option.pp "%a" (fun fs (src : Llair.Block.t) -> - Format.fprintf fs " #%i %s" src.sort_index src.lbl )) - src + let pop_throw stk ~init ~unwind = + let rec pop_throw_ state = function + | Return {params; locals; from_call; stk} -> + pop_throw_ (unwind params locals from_call state) stk + | Throw (dst, Return {from_call; stk}) -> + Some (from_call, dst, stk, state) + | Empty -> None + | Throw _ as stk -> violates invariant stk + in + pop_throw_ init stk end - module Depths = struct - type t = int Map.M(Edge).t + module Work : sig + type t + + val init : Dom.t -> Llair.block -> int -> t + + type x + + val skip : x + val seq : x -> x -> x + + val add : + ?prev:Llair.block + -> retreating:bool + -> Stack.t + -> Dom.t + -> Llair.block + -> x + + val run : f:(Stack.t -> Dom.t -> Llair.block -> x) -> t -> unit + end = struct + module Edge = struct + module T = struct + type t = + { dst: Llair.Block.t + ; src: Llair.Block.t option + ; stk: Stack.as_inlined_location } + [@@deriving compare, sexp_of] + end + + include T + include Comparator.Make (T) + + let pp fs {dst; src} = + Format.fprintf fs "#%i %s <--%a" dst.sort_index dst.lbl + (Option.pp "%a" (fun fs (src : Llair.Block.t) -> + Format.fprintf fs " #%i %s" src.sort_index src.lbl )) + src + end - let empty = Map.empty (module Edge) - let find = Map.find - let set = Map.set + module Depths = struct + type t = int Map.M(Edge).t - let join x y = - Map.merge x y ~f:(fun ~key:_ -> function - | `Left d | `Right d -> Some d - | `Both (d1, d2) -> Some (Int.max d1 d2) ) - end + let empty = Map.empty (module Edge) + let find = Map.find + let set = Map.set - type priority = int * Edge.t [@@deriving compare] - type priority_queue = priority Fheap.t - type waiting_states = (Domain.t * Depths.t) list Map.M(Llair.Block).t - type t = priority_queue * waiting_states * int - type x = Depths.t -> t -> t + let join x y = + Map.merge x y ~f:(fun ~key:_ -> function + | `Left d | `Right d -> Some d + | `Both (d1, d2) -> Some (Int.max d1 d2) ) + end - let empty_waiting_states : waiting_states = Map.empty (module Llair.Block) - let pp_priority fs (n, e) = Format.fprintf fs "%i: %a" n Edge.pp e + type priority = int * Edge.t [@@deriving compare] + type priority_queue = priority Fheap.t + type waiting_states = (Dom.t * Depths.t) list Map.M(Llair.Block).t + type t = priority_queue * waiting_states * int + type x = Depths.t -> t -> t + + let empty_waiting_states : waiting_states = + Map.empty (module Llair.Block) + + let pp_priority fs (n, e) = Format.fprintf fs "%i: %a" n Edge.pp e + + let pp fs pq = + Format.fprintf fs "@[%a@]" + (List.pp " ::@ " pp_priority) + (Sequence.to_list (Fheap.to_sequence pq)) + + let skip _ w = w + let seq x y d w = y d (x d w) + + let add ?prev ~retreating stk state curr depths ((pq, ws, bound) as work) + = + let edge = {Edge.dst= curr; src= prev; stk} in + let depth = Option.value (Depths.find depths edge) ~default:0 in + let depth = if retreating then depth + 1 else depth in + if depth > bound then ( + [%Trace.info "prune: %i: %a" depth Edge.pp edge] ; + work ) + else + let pq = Fheap.add pq (depth, edge) in + [%Trace.info "@[<6>enqueue %i: %a@ | %a@]" depth Edge.pp edge pp pq] ; + let depths = Depths.set depths ~key:edge ~data:depth in + let ws = Map.add_multi ws ~key:curr ~data:(state, depths) in + (pq, ws, bound) + + let init state curr bound = + add ~retreating:false Stack.empty state curr Depths.empty + (Fheap.create ~cmp:compare_priority, empty_waiting_states, bound) + + let rec run ~f (pq0, ws, bnd) = + match Fheap.pop pq0 with + | Some ((_, ({Edge.dst; stk} as edge)), pq) -> ( + match Map.find_and_remove ws dst with + | Some (state :: states, ws) -> + let join (qa, da) (q, d) = (Dom.join q qa, Depths.join d da) in + let qs, depths = List.fold ~f:join ~init:state states in + run ~f (f stk qs dst depths (pq, ws, bnd)) + | _ -> + [%Trace.info "done: %a" Edge.pp edge] ; + run ~f (pq, ws, bnd) ) + | None -> [%Trace.info "queue empty"] ; () + end - let pp fs pq = - Format.fprintf fs "@[%a@]" - (List.pp " ::@ " pp_priority) - (Sequence.to_list (Fheap.to_sequence pq)) + let exec_jump stk state block Llair.{dst; retreating} = + Work.add ~prev:block ~retreating stk state dst - let skip _ w = w - let seq x y d w = y d (x d w) + let summary_table = Hashtbl.create (module Var) - let add ?prev ~retreating stk state curr depths ((pq, ws, bound) as work) - = - let edge = {Edge.dst= curr; src= prev; stk} in - let depth = Option.value (Depths.find depths edge) ~default:0 in - let depth = if retreating then depth + 1 else depth in - if depth > bound then ( - [%Trace.info "prune: %i: %a" depth Edge.pp edge] ; - work ) - else - let pq = Fheap.add pq (depth, edge) in - [%Trace.info "@[<6>enqueue %i: %a@ | %a@]" depth Edge.pp edge pp pq] ; - let depths = Depths.set depths ~key:edge ~data:depth in - let ws = Map.add_multi ws ~key:curr ~data:(state, depths) in - (pq, ws, bound) - - let init state curr bound = - add ~retreating:false Stack.empty state curr Depths.empty - (Fheap.create ~cmp:compare_priority, empty_waiting_states, bound) - - let rec run ~f (pq0, ws, bnd) = - match Fheap.pop pq0 with - | Some ((_, ({Edge.dst; stk} as edge)), pq) -> ( - match Map.find_and_remove ws dst with - | Some (state :: states, ws) -> - let join (qa, da) (q, d) = (Domain.join q qa, Depths.join d da) in - let qs, depths = List.fold ~f:join ~init:state states in - run ~f (f stk qs dst depths (pq, ws, bnd)) - | _ -> - [%Trace.info "done: %a" Edge.pp edge] ; - run ~f (pq, ws, bnd) ) - | None -> [%Trace.info "queue empty"] ; () -end + let exec_call opts stk state block call globals = + let Llair.{callee; args; areturn; return; recursive} = call in + let Llair.{name; params; freturn; locals; entry} = callee in + [%Trace.call fun {pf} -> + pf "%a from %a" Var.pp name.var Var.pp return.dst.parent.name.var] + ; + let dnf_states = + 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 + in + List.fold ~init:Work.skip dnf_states ~f:(fun acc state -> + match + if not opts.function_summaries then None + else + let maybe_summary_post = + let state = fst (domain_call ~summaries:false state) in + Hashtbl.find summary_table name.var + >>= List.find_map ~f:(Dom.apply_summary state) + in + [%Trace.info + "Maybe summary post: %a" (Option.pp "%a" Dom.pp) + maybe_summary_post] ; + maybe_summary_post + with + | None -> + let state, from_call = + domain_call ~summaries:opts.function_summaries state + in + Work.seq acc + ( match + Stack.push_call call ~bound:opts.bound from_call stk + with + | Some stk -> + Work.add stk ~prev:block ~retreating:recursive state entry + | None -> Work.skip ) + | Some post -> Work.seq acc (exec_jump stk post block return) ) + |> + [%Trace.retn fun {pf} _ -> pf ""] + + let pp_st () = + [%Trace.printf + "@[%t@]" (fun fs -> + Hashtbl.iteri summary_table ~f:(fun ~key ~data -> + Format.fprintf fs "@[%a:@ @[%a@]@]@ " Var.pp key + (List.pp "@," Dom.pp_summary) + data ) )] + + let exec_return ~opts stk pre_state (block : Llair.block) exp globals = + let Llair.{name; params; freturn; locals} = block.parent in + [%Trace.call fun {pf} -> pf "from %a" Var.pp name.var] + ; + ( 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 retn_state = Dom.retn params freturn from_call post_state in + exec_jump stk retn_state block retn_site + | None -> Work.skip ) + |> + [%Trace.retn fun {pf} _ -> pf ""] -let exec_jump stk state block Llair.{dst; retreating} = - Work.add ~prev:block ~retreating stk state dst - -let summary_table = Hashtbl.create (module Var) - -let exec_call opts stk state block call globals = - let Llair.{callee; args; areturn; return; recursive} = call in - let Llair.{name; params; freturn; locals; entry} = callee in - [%Trace.call fun {pf} -> - pf "%a from %a" Var.pp name.var Var.pp return.dst.parent.name.var] - ; - let dnf_states = - if opts.function_summaries then Domain.dnf state else [state] - in - let domain_call = - Domain.call args areturn params (Set.add_option freturn locals) globals - in - List.fold ~init:Work.skip dnf_states ~f:(fun acc state -> - match - if not opts.function_summaries then None - else - let maybe_summary_post = - let state = fst (domain_call ~summaries:false state) in - Hashtbl.find summary_table name.var - >>= List.find_map ~f:(Domain.apply_summary state) - in - [%Trace.info - "Maybe summary post: %a" - (Option.pp "%a" Domain.pp) - maybe_summary_post] ; - maybe_summary_post - with - | None -> - let state, from_call = - domain_call ~summaries:opts.function_summaries state - in - Work.seq acc - ( match Stack.push_call call ~bound:opts.bound from_call stk with - | Some stk -> - Work.add stk ~prev:block ~retreating:recursive state entry - | None -> Work.skip ) - | Some post -> Work.seq acc (exec_jump stk post block return) ) - |> - [%Trace.retn fun {pf} _ -> pf ""] - -let pp_st () = - [%Trace.printf - "@[%t@]" (fun fs -> - Hashtbl.iteri summary_table ~f:(fun ~key ~data -> - Format.fprintf fs "@[%a:@ @[%a@]@]@ " Var.pp key - (List.pp "@," State_domain.pp_function_summary) - data ) )] - -let exec_return ~opts stk pre_state (block : Llair.block) exp globals = - let Llair.{name; params; freturn; locals} = block.parent in - [%Trace.call fun {pf} -> pf "from %a" Var.pp name.var] - ; - ( match Stack.pop_return stk with - | Some (from_call, retn_site, stk) -> - let exit_state = - match (freturn, exp) with - | Some freturn, Some return_val -> - Domain.exec_move pre_state freturn return_val - | None, None -> pre_state - | _ -> violates Llair.Func.invariant block.parent - in - let post_state = Domain.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 = - Domain.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 retn_state = Domain.retn params freturn from_call post_state in - exec_jump stk retn_state block retn_site - | None -> Work.skip ) - |> - [%Trace.retn fun {pf} _ -> pf ""] - -let exec_throw stk pre_state (block : Llair.block) exc = - let func = block.parent in - [%Trace.call fun {pf} -> pf "from %a" Var.pp func.name.var] - ; - let unwind params scope from_call state = - Domain.retn params (Some func.fthrow) from_call - (Domain.post scope from_call state) - in - ( match Stack.pop_throw stk ~unwind ~init:pre_state with - | Some (from_call, retn_site, stk, unwind_state) -> - let fthrow = func.fthrow in - let exit_state = Domain.exec_move unwind_state fthrow exc in - let post_state = Domain.post func.locals from_call exit_state in - let retn_state = - Domain.retn func.params func.freturn from_call post_state - in - exec_jump stk retn_state block retn_site - | None -> Work.skip ) - |> - [%Trace.retn fun {pf} _ -> pf ""] - -let exec_skip_func : - Stack.t - -> Domain.t - -> Llair.block - -> Var.t option - -> Llair.jump - -> Work.x = - fun stk state block areturn return -> - Report.unknown_call block.term ; - let state = Option.fold ~f:Domain.exec_kill ~init:state areturn in - exec_jump stk state block return - -let exec_term : - exec_opts -> Llair.t -> Stack.t -> Domain.t -> Llair.block -> Work.x = - fun opts pgm stk state block -> - [%Trace.info "exec %a" Llair.Term.pp block.term] ; - match block.term with - | Switch {key; tbl; els} -> - Vector.fold tbl - ~f:(fun x (case, jump) -> - match Domain.exec_assume state (Exp.eq key case) with - | Some state -> exec_jump stk state block jump |> Work.seq x - | None -> x ) - ~init: - ( match - Domain.exec_assume state - (Vector.fold tbl ~init:(Exp.bool true) - ~f:(fun b (case, _) -> Exp.and_ (Exp.dq key case) b)) - with - | Some state -> exec_jump stk state block els - | None -> Work.skip ) - | Iswitch {ptr; tbl} -> - Vector.fold tbl ~init:Work.skip ~f:(fun x (jump : Llair.jump) -> - match - Domain.exec_assume state - (Exp.eq ptr - (Exp.label - ~parent:(Var.name jump.dst.parent.name.var) - ~name:jump.dst.lbl)) - with - | Some state -> exec_jump stk state block jump |> Work.seq x - | None -> x ) - | Call ({callee; args; areturn; return} as call) -> ( - match - let lookup name = - Option.to_list (Llair.Func.find pgm.functions name) - in - Domain.resolve_callee lookup callee state - with - | [] -> exec_skip_func stk state block areturn return - | callees -> - List.fold callees ~init:Work.skip ~f:(fun x callee -> + let exec_throw stk pre_state (block : Llair.block) exc = + let func = block.parent in + [%Trace.call fun {pf} -> pf "from %a" Var.pp func.name.var] + ; + let unwind params scope from_call state = + Dom.retn params (Some func.fthrow) from_call + (Dom.post scope from_call state) + in + ( match Stack.pop_throw stk ~unwind ~init:pre_state with + | Some (from_call, retn_site, stk, unwind_state) -> + let fthrow = func.fthrow in + let exit_state = Dom.exec_move unwind_state fthrow exc in + let post_state = Dom.post func.locals from_call exit_state in + let retn_state = + Dom.retn func.params func.freturn from_call post_state + in + exec_jump stk retn_state block retn_site + | None -> Work.skip ) + |> + [%Trace.retn fun {pf} _ -> pf ""] + + let exec_skip_func : + Stack.t + -> Dom.t + -> Llair.block + -> Var.t option + -> Llair.jump + -> Work.x = + fun stk state block areturn return -> + Report.unknown_call block.term ; + let state = Option.fold ~f:Dom.exec_kill ~init:state areturn in + exec_jump stk state block return + + let exec_term : + exec_opts -> Llair.t -> Stack.t -> Dom.t -> Llair.block -> Work.x = + fun opts pgm stk state block -> + [%Trace.info "exec %a" Llair.Term.pp block.term] ; + match block.term with + | Switch {key; tbl; els} -> + Vector.fold tbl + ~f:(fun x (case, jump) -> + match Dom.exec_assume state (Exp.eq key case) with + | Some state -> exec_jump stk state block jump |> Work.seq x + | None -> x ) + ~init: ( match - Domain.exec_intrinsic ~skip_throw:opts.skip_throw state - areturn callee.name.var args + Dom.exec_assume state + (Vector.fold tbl ~init:(Exp.bool true) + ~f:(fun b (case, _) -> Exp.and_ (Exp.dq key case) b)) with - | Some (Error ()) -> - Report.invalid_access_term (Domain.project state) block.term ; - Work.skip - | Some (Ok state) when Domain.is_false state -> Work.skip - | Some (Ok state) -> exec_jump stk state block return - | None when Llair.Func.is_undefined callee -> - exec_skip_func stk state block areturn return - | None -> - exec_call opts stk state block {call with callee} - pgm.globals ) - |> Work.seq x ) ) - | Return {exp} -> exec_return ~opts stk state block exp pgm.globals - | Throw {exc} -> - if opts.skip_throw then Work.skip else exec_throw stk state block exc - | Unreachable -> Work.skip - -let exec_inst : - Domain.t -> Llair.inst -> (Domain.t, Domain.t * Llair.inst) result = - fun state inst -> - Domain.exec_inst state inst - |> Result.map_error ~f:(fun () -> (state, inst)) - -let exec_block : - exec_opts -> Llair.t -> Stack.t -> Domain.t -> Llair.block -> Work.x = - fun opts pgm stk state block -> - [%Trace.info "exec %a" Llair.Block.pp block] ; - match Vector.fold_result ~f:exec_inst ~init:state block.cmnd with - | Ok state -> exec_term opts pgm stk state block - | Error (state, inst) -> - Report.invalid_access_inst (Domain.project state) inst ; - Work.skip - -let harness : exec_opts -> Llair.t -> (int -> Work.t) option = - 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) ) - |> function - | Some {locals; params= []; entry} -> - Some - (Work.init - (fst - (Domain.call ~summaries:opts.function_summaries [] None [] - locals pgm.globals (Domain.init pgm.globals))) - entry) - | _ -> None - -let exec_pgm : exec_opts -> Llair.t -> unit = - fun opts pgm -> - [%Trace.call fun {pf} -> pf "@]@,@["] - ; - ( match harness opts pgm with - | Some work -> Work.run ~f:(exec_block opts pgm) (work opts.bound) - | None -> fail "no applicable harness" () ) - |> - [%Trace.retn fun {pf} _ -> pf ""] + | Some state -> exec_jump stk state block els + | None -> Work.skip ) + | Iswitch {ptr; tbl} -> + Vector.fold tbl ~init:Work.skip ~f:(fun x (jump : Llair.jump) -> + match + Dom.exec_assume state + (Exp.eq ptr + (Exp.label + ~parent:(Var.name jump.dst.parent.name.var) + ~name:jump.dst.lbl)) + with + | Some state -> exec_jump stk state block jump |> Work.seq x + | None -> x ) + | Call ({callee; args; areturn; return} as call) -> ( + match + let lookup name = + Option.to_list (Llair.Func.find pgm.functions name) + in + Dom.resolve_callee lookup callee state + with + | [] -> exec_skip_func stk state block areturn return + | callees -> + List.fold callees ~init:Work.skip ~f:(fun x callee -> + ( match + Dom.exec_intrinsic ~skip_throw:opts.skip_throw state + areturn callee.name.var args + with + | Some (Error ()) -> + Report.invalid_access_term + (Dom.report_fmt_thunk state) + block.term ; + Work.skip + | Some (Ok state) when Dom.is_false state -> Work.skip + | Some (Ok state) -> exec_jump stk state block return + | None when Llair.Func.is_undefined callee -> + exec_skip_func stk state block areturn return + | None -> + exec_call opts stk state block {call with callee} + pgm.globals ) + |> Work.seq x ) ) + | Return {exp} -> exec_return ~opts stk state block exp pgm.globals + | Throw {exc} -> + if opts.skip_throw then Work.skip + else exec_throw stk state block exc + | Unreachable -> Work.skip + + let exec_inst : Dom.t -> Llair.inst -> (Dom.t, Dom.t * Llair.inst) result + = + fun state inst -> + Dom.exec_inst state inst + |> Result.map_error ~f:(fun () -> (state, inst)) + + let exec_block : + exec_opts -> Llair.t -> Stack.t -> Dom.t -> Llair.block -> Work.x = + fun opts pgm stk state block -> + [%Trace.info "exec %a" Llair.Block.pp block] ; + match Vector.fold_result ~f:exec_inst ~init:state block.cmnd with + | Ok state -> exec_term opts pgm stk state block + | Error (state, inst) -> + Report.invalid_access_inst (Dom.report_fmt_thunk state) inst ; + Work.skip + + let harness : exec_opts -> Llair.t -> (int -> Work.t) option = + 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) ) + |> function + | Some {locals; params= []; entry} -> + Some + (Work.init + (fst + (Dom.call ~summaries:opts.function_summaries [] None [] + locals pgm.globals (Dom.init pgm.globals))) + entry) + | _ -> None + + let exec_pgm : exec_opts -> Llair.t -> unit = + fun opts pgm -> + [%Trace.call fun {pf} -> pf "@]@,@["] + ; + ( match harness opts pgm with + | Some work -> Work.run ~f:(exec_block opts pgm) (work opts.bound) + | None -> fail "no applicable harness" () ) + |> + [%Trace.retn fun {pf} _ -> pf ""] +end diff --git a/sledge/src/control.mli b/sledge/src/control.mli index 95f3febf3..5ab2d6f4d 100644 --- a/sledge/src/control.mli +++ b/sledge/src/control.mli @@ -12,4 +12,6 @@ type exec_opts = ; skip_throw: bool (** Treat throw as unreachable *) ; function_summaries: bool (** Use function summarisation *) } -val exec_pgm : exec_opts -> Llair.t -> unit +module Make (Dom : Domain_sig.Dom) : sig + val exec_pgm : exec_opts -> Llair.t -> unit +end diff --git a/sledge/src/domain_sig.ml b/sledge/src/domain_sig.ml new file mode 100644 index 000000000..b400994eb --- /dev/null +++ b/sledge/src/domain_sig.ml @@ -0,0 +1,57 @@ +(* + * 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. + *) + +(** Abstract Domain *) +module type Dom = sig + type t + + val pp : t pp + val report_fmt_thunk : t -> Formatter.t -> unit + val init : Global.t vector -> t + val join : t -> t -> t + val is_false : t -> bool + val exec_assume : t -> Exp.t -> t option + val exec_kill : t -> Var.t -> t + val exec_move : t -> Var.t -> Exp.t -> t + val exec_inst : t -> Llair.inst -> (t, unit) result + + val exec_intrinsic : + skip_throw:bool + -> t + -> Var.t option + -> Var.t + -> Exp.t list + -> (t, unit) result option + + type from_call [@@deriving sexp_of] + + val call : + summaries:bool + -> Exp.t list + -> Var.t option + -> Var.t list + -> Var.Set.t + -> Global.t vector + -> t + -> t * from_call + + val post : Var.Set.t -> from_call -> t -> t + val retn : Var.t list -> Var.t option -> from_call -> t -> t + val dnf : t -> t list + + val resolve_callee : + (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list + + type summary + + val pp_summary : summary pp + + val create_summary : + locals:Var.Set.t -> formals:Var.Set.t -> t -> summary * t + + val apply_summary : t -> summary -> t option +end diff --git a/sledge/src/report.ml b/sledge/src/report.ml index 8324f16e0..0e8dde708 100644 --- a/sledge/src/report.ml +++ b/sledge/src/report.ml @@ -22,18 +22,17 @@ let unknown_call call = | _ -> () ) call Llair.Term.pp call] -let invalid_access state pp access loc = +let invalid_access fmt_thunk pp access loc = let rep fs = Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Loc.pp (loc access) pp access in Format.printf "@\n@[%t@]@." rep ; - [%Trace.printf - "@\n@[%t@;<1 2>@[{ %a@ }@]@]@." rep State_domain.pp state] ; + [%Trace.printf "@\n@[%t@;<1 2>@[{ %t@ }@]@]@." rep fmt_thunk] ; Stop.on_invalid_access () -let invalid_access_inst state inst = - invalid_access state Llair.Inst.pp inst Llair.Inst.loc +let invalid_access_inst fmt_thunk inst = + invalid_access fmt_thunk Llair.Inst.pp inst Llair.Inst.loc -let invalid_access_term state term = - invalid_access state Llair.Term.pp term Llair.Term.loc +let invalid_access_term fmt_thunk term = + invalid_access fmt_thunk Llair.Term.pp term Llair.Term.loc diff --git a/sledge/src/report.mli b/sledge/src/report.mli index 8daccdb58..04a8482e7 100644 --- a/sledge/src/report.mli +++ b/sledge/src/report.mli @@ -8,5 +8,5 @@ (** Issue reporting *) val unknown_call : Llair.term -> unit -val invalid_access_inst : State_domain.t -> Llair.inst -> unit -val invalid_access_term : State_domain.t -> Llair.term -> unit +val invalid_access_inst : (Formatter.t -> unit) -> Llair.inst -> unit +val invalid_access_term : (Formatter.t -> unit) -> Llair.term -> unit diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml index 59cde5860..09a0200c1 100644 --- a/sledge/src/sledge.ml +++ b/sledge/src/sledge.ml @@ -13,6 +13,9 @@ open Command.Let_syntax type 'a param = 'a Command.Param.t +module Sh_executor = Control.Make (Sh_domain) +module Unit_executor = Control.Make (Unit_domain) + (* reverse application in the Command.Param applicative *) let ( |*> ) : 'a param -> ('a -> 'b) param -> 'b param = fun x f -> x |> Command.Param.apply f @@ -75,9 +78,15 @@ 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 in fun program () -> - Control.exec_pgm {bound; skip_throw; function_summaries} (program ()) + exec {bound; skip_throw; function_summaries} (program ()) let analyze_cmd = let summary = "analyze LLAIR code" in diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/sh_domain.ml similarity index 95% rename from sledge/src/symbheap/domain.ml rename to sledge/src/symbheap/sh_domain.ml index dcd25398e..195868b8e 100644 --- a/sledge/src/symbheap/domain.ml +++ b/sledge/src/symbheap/sh_domain.ml @@ -10,12 +10,12 @@ type t = State_domain.t * State_domain.t let embed q = (q, q) -let project (_, curr) = curr let pp fs (entry, current) = Format.fprintf fs "@[ entry: %a@;current: %a@]" State_domain.pp entry State_domain.pp current +let report_fmt_thunk (_, curr) fs = State_domain.pp fs curr let init globals = embed (State_domain.init globals) let join (entry_a, current_a) (entry_b, current_b) = @@ -95,6 +95,10 @@ let dnf (entry, current) = let resolve_callee f e (_, current) = State_domain.resolve_callee f e current +type summary = State_domain.summary + +let pp_summary = State_domain.pp_summary + let create_summary ~locals ~formals (entry, current) = let fs, current = State_domain.create_summary ~locals ~formals ~entry ~current diff --git a/sledge/src/symbheap/domain.mli b/sledge/src/symbheap/sh_domain.mli similarity index 85% rename from sledge/src/symbheap/domain.mli rename to sledge/src/symbheap/sh_domain.mli index 5fc8bd2ef..37e86c096 100644 --- a/sledge/src/symbheap/domain.mli +++ b/sledge/src/symbheap/sh_domain.mli @@ -9,8 +9,8 @@ type t -val project : t -> State_domain.t val pp : t pp +val report_fmt_thunk : t -> Formatter.t -> unit val init : Global.t vector -> t val join : t -> t -> t val is_false : t -> bool @@ -28,16 +28,16 @@ val exec_intrinsic : -> (t, unit) result option type from_call [@@deriving sexp_of] +type summary + +val pp_summary : summary pp (* formals should include all the parameters of the summary. That is both formals and globals.*) val create_summary : - locals:Var.Set.t - -> formals:Var.Set.t - -> t - -> State_domain.function_summary * t + locals:Var.Set.t -> formals:Var.Set.t -> t -> summary * t -val apply_summary : t -> State_domain.function_summary -> t option +val apply_summary : t -> summary -> t option val call : summaries:bool diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml index 86a32746e..17349751c 100644 --- a/sledge/src/symbheap/state_domain.ml +++ b/sledge/src/symbheap/state_domain.ml @@ -152,9 +152,9 @@ let resolve_callee lookup ptr _ = | Some callee_name -> lookup callee_name | None -> [] -type function_summary = {xs: Var.Set.t; foot: t; post: t} +type summary = {xs: Var.Set.t; foot: t; post: t} -let pp_function_summary fs {xs; foot; post} = +let pp_summary fs {xs; foot; post} = Format.fprintf fs "@[xs: @[%a@]@ foot: %a@ post: %a @]" Var.Set.pp xs pp foot pp post @@ -184,10 +184,10 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) = let current = Sh.extend_us xs post in ({xs; foot; post}, current) |> - [%Trace.retn fun {pf} (fs, _) -> pf "@,%a" pp_function_summary fs] + [%Trace.retn fun {pf} (fs, _) -> pf "@,%a" pp_summary fs] let apply_summary ({xs; foot; post} as fs) q = - [%Trace.call fun {pf} -> pf "fs: %a@ q: %a" pp_function_summary fs pp q] + [%Trace.call fun {pf} -> pf "fs: %a@ q: %a" pp_summary fs pp q] ; let xs_in_q = Set.inter xs q.Sh.us in let xs_in_fv_q = Set.inter xs (Sh.fv q) in diff --git a/sledge/src/symbheap/state_domain.mli b/sledge/src/symbheap/state_domain.mli index e9ec91468..82c3cd3a7 100644 --- a/sledge/src/symbheap/state_domain.mli +++ b/sledge/src/symbheap/state_domain.mli @@ -38,10 +38,10 @@ val call : -> t -> t * from_call -type function_summary = {xs: Var.Set.t; foot: t; post: t} +type summary = {xs: Var.Set.t; foot: t; post: t} -val pp_function_summary : Format.formatter -> function_summary -> unit -val apply_summary : function_summary -> t -> t option +val pp_summary : summary pp +val apply_summary : summary -> t -> t option (* formals should include all the parameters of the summary. That is both formals and globals.*) @@ -50,7 +50,7 @@ val create_summary : -> formals:Var.Set.t -> entry:t -> current:t - -> function_summary * t + -> summary * t val post : Var.Set.t -> t -> t val retn : Var.t list -> Var.t option -> from_call -> t -> t diff --git a/sledge/src/unit_domain.ml b/sledge/src/unit_domain.ml new file mode 100644 index 000000000..d026ff7d3 --- /dev/null +++ b/sledge/src/unit_domain.ml @@ -0,0 +1,39 @@ +(* + * 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. + *) + +(** "Unit" abstract domain *) + +type t = unit + +let pp fs () = Format.pp_print_string fs "()" +let report_fmt_thunk () fs = pp fs () +let init _ = () +let join () () = () +let is_false _ = false +let exec_assume () _ = Some () +let exec_kill () _ = () +let exec_move () _ _ = () +let exec_inst () _ = Ok () +let exec_intrinsic ~skip_throw:_ _ _ _ _ : (t, unit) result option = None + +type from_call = unit [@@deriving compare, equal, sexp] + +let call ~summaries:_ _ _ _ _ _ _ = ((), ()) +let post _ _ () = () +let retn _ _ _ _ = () +let dnf () = [()] + +let resolve_callee lookup ptr _ = + match Var.of_exp ptr with + | Some callee_name -> lookup callee_name + | None -> [] + +type summary = unit + +let pp_summary fs () = Format.pp_print_string fs "()" +let create_summary ~locals:_ ~formals:_ _ = ((), ()) +let apply_summary _ _ = Some () diff --git a/sledge/src/unit_domain.mli b/sledge/src/unit_domain.mli new file mode 100644 index 000000000..93f619c01 --- /dev/null +++ b/sledge/src/unit_domain.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. + *) + +(** "Unit" abstract domain *) + +include Domain_sig.Dom