From b712a57bf999f84668e0e629ff314165a497d984 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 12 Oct 2018 09:04:39 -0700 Subject: [PATCH] [sledge] Add analysis based on iterative bounded exploration Reviewed By: mbouaziz Differential Revision: D9846736 fbshipit-source-id: 3c3a687b3 --- sledge/src/control.ml | 271 +++++++++++++++++++++++++++++++++++++++++ sledge/src/control.mli | 10 ++ 2 files changed, 281 insertions(+) create mode 100644 sledge/src/control.ml create mode 100644 sledge/src/control.mli diff --git a/sledge/src/control.ml b/sledge/src/control.ml new file mode 100644 index 000000000..c2395a3da --- /dev/null +++ b/sledge/src/control.ml @@ -0,0 +1,271 @@ +(* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** Iterative Breadth-First Bounded Exploration + + The analysis' semantics of control flow. *) + +let bound = 10 + +type stack = + | Locals of Var.Set.t * stack + | Return of Llair.Jump.t * Domain.from_call * stack + | Throw of Llair.Jump.t * stack + | Empty +[@@deriving compare, sexp_of] + +module Work : sig + type t + + val init : Domain.t -> Llair.block -> t + + type x + + val skip : x + val seq : x -> x -> x + + val add : + ?prev:Llair.block + -> retreating:bool + -> stack + -> Domain.t + -> Llair.block + -> x + + val run : f:(stack -> 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} + [@@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 + + module Depths = struct + type t = int Map.M(Edge).t + + let empty = Map.empty (module Edge) + let find = Map.find + let set = Map.set + + let join x y = + Map.merge x y ~f:(fun ~key:_ -> function + | `Left d | `Right d -> Some d + | `Both (d1, d2) -> Some (Int.min d1 d2) ) + end + + 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 + type x = Depths.t -> t -> t + + let empty_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) 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) + + let init state curr = + add ~retreating:false Empty state curr Depths.empty + (Fheap.create ~cmp:compare_priority, empty_waiting_states) + + let rec run ~f (pq0, ws) = + 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)) + | _ -> + [%Trace.info "done: %a" Edge.pp edge] ; + run ~f (pq, ws) ) + | None -> [%Trace.info "queue empty"] ; () +end + +let push_jump lcls stk = + if Set.is_empty lcls then stk else Locals (lcls, stk) + +let exec_jump stk state block ({dst; args; retreating} : Llair.jump) = + let state, _ = Domain.call state args dst.params dst.locals in + let stk = push_jump dst.locals stk in + Work.add ~prev:block ~retreating stk state dst + +let push_call locals ~return from_call ?throw stk = + let push_return jmp from_call stk = Return (jmp, from_call, stk) in + let push_throw jmp stk = + match jmp with Some jmp -> Throw (jmp, stk) | None -> stk + in + push_jump locals (push_return return from_call (push_throw throw stk)) + +let exec_call stk state block ({dst; args; retreating} : Llair.jump) return + throw = + let state, from_call = Domain.call state args dst.params dst.locals in + let stk = push_call dst.locals ~return from_call ?throw stk in + Work.add stk ~prev:block ~retreating state dst + +let pop_return stk ~init ~f = + let rec pop_return_ scope = function + | Locals (locals, stk) -> pop_return_ (Set.union locals scope) stk + | Return (jmp, from_call, stk) -> Some (stk, f scope from_call init, jmp) + | _ -> None + in + pop_return_ Var.Set.empty stk + +let exec_return stk state block exp = + match pop_return stk ~init:state ~f:Domain.retn with + | Some (stk, state, ({args} as jmp)) -> + exec_jump stk state block {jmp with args= Option.cons exp args} + | None -> Work.skip + +let rec pop_throw stk ~init ~f = + match pop_return stk ~init ~f with + | Some (stk, state, _) -> pop_throw stk ~init:state ~f + | None -> ( + match stk with Throw (jmp, stk) -> Some (stk, init, jmp) | _ -> None ) + +let exec_throw stk state block exc = + match pop_throw stk ~init:state ~f:Domain.retn with + | Some (stk, state, ({args} as jmp)) -> + exec_jump stk state block {jmp with args= exc :: args} + | None -> Work.skip + +let exec_skip_func stk state block ({dst; args} as return : Llair.jump) = + let return = + if List.is_empty dst.params then return + else + let args = + List.fold_right dst.params ~init:args ~f:(fun param args -> + Exp.nondet (Var.name param) :: args ) + in + {return with args} + in + exec_jump stk state block return + +let exec_term : Llair.t -> stack -> Domain.t -> Llair.block -> Work.x = + fun 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.assume state (Exp.eq key (Exp.integer case)) with + | Some state -> exec_jump stk state block jump |> Work.seq x + | None -> x ) + ~init: + ( match + Domain.assume state + (Vector.fold tbl ~init:(Exp.bool true) + ~f:(fun b (case, _) -> + Exp.and_ (Exp.dq key (Exp.integer 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.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 {call= {dst; args; retreating}; return; throw} -> ( + match + let lookup name = + Option.to_list (Llair.Func.find pgm.functions name) + in + Domain.resolve_callee lookup dst state + with + | [] -> exec_skip_func stk state block return + | callees -> + List.fold callees ~init:Work.skip ~f:(fun x callee -> + ( if Llair.Func.is_undefined callee then + exec_skip_func stk state block return + else + exec_call stk state block + {dst= callee.entry; args; retreating} + return throw ) + |> Work.seq x ) ) + | Return {exp} -> exec_return stk state block exp + | Throw {exc} -> exec_throw stk state block exc + | Unreachable -> Work.skip + +let exec_block : Llair.t -> stack -> Domain.t -> Llair.block -> Work.x = + fun pgm stk state block -> + [%Trace.info "exec %a" Llair.Block.pp block] ; + match Vector.fold_result ~f:Domain.exec_inst ~init:state block.cmnd with + | Ok state -> exec_term pgm stk state block + | Error (q, i) -> + Format.printf + "@\n\ + @[%a Invalid memory access executing instruction@;<1 \ + 2>@[%a@]%t@]@." + Loc.pp (Llair.Inst.loc i) Llair.Inst.pp i (fun fs -> + if Version.debug then + Format.fprintf fs "@ from symbolic state@;<1 2>@[%a@]" Domain.pp + q ) ; + Work.skip + +let harness : Llair.t -> Work.t option = + fun pgm -> + List.find_map ["__llair_main"; "_Z12__llair_mainv"; "main"] + ~f:(fun name -> + Vector.find_map pgm.functions ~f:(fun func -> + let fname = Var.name func.name.var in + Option.some_if (String.equal name fname) (fname, func) ) ) + |> function + | Some (("__llair_main" | "_Z12__llair_mainv" | "main"), main) -> + let block = main.entry in + if List.is_empty block.params then + Some + (Work.init + (fst (Domain.call (Domain.init pgm.globals) [] [] block.locals)) + block) + else None + | _ -> None + +let exec_pgm : Llair.t -> unit = + fun pgm -> + [%Trace.call fun {pf} -> pf "@]@,@["] + ; + ( match harness pgm with + | Some work -> Work.run ~f:(exec_block pgm) work + | None -> fail "no applicable harness" () ) + |> + [%Trace.retn fun {pf} _ -> pf ""] diff --git a/sledge/src/control.mli b/sledge/src/control.mli new file mode 100644 index 000000000..bfdbc3da7 --- /dev/null +++ b/sledge/src/control.mli @@ -0,0 +1,10 @@ +(* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** The analysis' semantics of control flow. *) + +val exec_pgm : Llair.t -> unit