From ba6e6bf3699284b0850ec9636fd08a8c6a20fe7b Mon Sep 17 00:00:00 2001 From: Timotej Kapus Date: Mon, 15 Jul 2019 01:22:09 -0700 Subject: [PATCH] [sledge] Actually use function summaries Summary: If function summaries are enabled calling a function first tries to apply a summary, if succesful, it directly jumps to the return site of the call. Otherwise it proceeds as before. Reviewed By: jvillard Differential Revision: D16201251 fbshipit-source-id: cec52e0e5 --- sledge/src/control.ml | 54 ++++++++++++++-------------- sledge/src/symbheap/domain.ml | 7 ++-- sledge/src/symbheap/domain.mli | 4 +-- sledge/src/symbheap/state_domain.ml | 27 +++++++++++--- sledge/src/symbheap/state_domain.mli | 6 +++- 5 files changed, 63 insertions(+), 35 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 67718a847..87cf98208 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -253,7 +253,7 @@ let exec_jump ?temps stk state block ({dst; args} as jmp : Llair.jump) = let state = Domain.jump args dst.params ?temps state in exec_goto stk state block jmp -let caller_state_log = ref [] +let summary_table = Hashtbl.create (module Var) let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump) (return : Llair.jump) throw globals = @@ -264,28 +264,36 @@ let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump) let dnf_states = if opts.function_summaries then Domain.dnf state else [state] in + let locals = dst.parent.locals in + let domain_call = Domain.call args dst.params locals globals in List.fold ~init:Work.skip dnf_states ~f:(fun acc state -> - let locals = dst.parent.locals in - caller_state_log := - fst - (Domain.call ~summaries:false args dst.params locals globals state) - :: !caller_state_log ; - let state, from_call = - Domain.call ~summaries:opts.function_summaries args dst.params - locals globals state + let maybe_summary_post = + if opts.function_summaries then + let state = fst (domain_call ~summaries:false state) in + Hashtbl.find summary_table dst.parent.name.var + >>= List.find_map ~f:(Domain.apply_summary state) + else None in - Work.seq acc - ( match - Stack.push_call ~bound:opts.bound dst ~retreating ~return - from_call ?throw stk - with - | Some stk -> Work.add stk ~prev:block ~retreating state dst - | None -> Work.skip ) ) + [%Trace.info + "Maybe summary post: %a" + (Option.pp "%a" Domain.pp) + maybe_summary_post] ; + match maybe_summary_post with + | None -> + let state, from_call = + domain_call ~summaries:opts.function_summaries state + in + Work.seq acc + ( match + Stack.push_call ~bound:opts.bound dst ~retreating ~return + from_call ?throw stk + with + | Some stk -> Work.add stk ~prev:block ~retreating state dst + | None -> Work.skip ) + | Some post -> Work.seq acc (exec_goto stk post block return) ) |> [%Trace.retn fun {pf} _ -> pf ""] -let summary_table = Hashtbl.create (module Var) - let pp_st _ = [%Trace.printf "@[%t@]" (fun fs -> @@ -311,11 +319,10 @@ let exec_return ~opts stk pre_state (block : Llair.block) exp globals = Var.Set.of_vector (Vector.map globals ~f:(fun (g : Global.t) -> g.var)) in - let function_summary = - Domain.create_summary ~locals:block.parent.locals + let function_summary, exit_state = + Domain.create_summary ~locals:block.parent.locals exit_state ~formals: (Set.union (Var.Set.of_list block.parent.entry.params) globals) - exit_state in if opts.function_summaries then ( Hashtbl.add_multi summary_table ~key:block.parent.name.var @@ -327,11 +334,6 @@ let exec_return ~opts stk pre_state (block : Llair.block) exp globals = let retn_state = Domain.retn block.parent.entry.params from_call post_state in - let _ = - Domain.apply_summary function_summary - (List.hd_exn !caller_state_log) - in - caller_state_log := List.tl_exn !caller_state_log ; exec_jump stk retn_state block ~temps:(Option.fold ~f:Set.add freturn ~init:Var.Set.empty) ( match freturn with diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml index cc65b117e..a639b3841 100644 --- a/sledge/src/symbheap/domain.ml +++ b/sledge/src/symbheap/domain.ml @@ -94,9 +94,12 @@ let resolve_callee f e (_, current) = State_domain.resolve_callee f e current let create_summary ~locals ~formals (entry, current) = - State_domain.create_summary ~locals ~formals entry current + let fs, current = + State_domain.create_summary ~locals ~formals ~entry ~current + in + (fs, (entry, current)) -let apply_summary fs (entry, current) = +let apply_summary (entry, current) fs = Option.map ~f:(fun c -> (entry, c)) (State_domain.apply_summary fs current) diff --git a/sledge/src/symbheap/domain.mli b/sledge/src/symbheap/domain.mli index 5c732874b..581d3e124 100644 --- a/sledge/src/symbheap/domain.mli +++ b/sledge/src/symbheap/domain.mli @@ -34,9 +34,9 @@ val create_summary : locals:Var.Set.t -> formals:Var.Set.t -> t - -> State_domain.function_summary + -> State_domain.function_summary * t -val apply_summary : State_domain.function_summary -> t -> t option +val apply_summary : t -> State_domain.function_summary -> t option val jump : Exp.t list -> Var.t list -> ?temps:Var.Set.t -> t -> t val call : diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml index a03055cfd..113492951 100644 --- a/sledge/src/symbheap/state_domain.ml +++ b/sledge/src/symbheap/state_domain.ml @@ -177,7 +177,7 @@ let pp_function_summary fs {xs; foot; post} = Format.fprintf fs "@[xs: @[%a@]@ foot: %a@ post: %a @]" Var.Set.pp xs pp foot pp post -let create_summary ~locals ~formals entry current = +let create_summary ~locals ~formals ~entry ~current = [%Trace.call fun {pf} -> pf "formals %a@ entry: %a@ current: %a" Var.Set.pp formals pp entry pp current] @@ -201,16 +201,35 @@ let create_summary ~locals ~formals entry current = let xs_and_formals = Set.union xs formals in let foot = Sh.exists (Set.diff foot.us xs_and_formals) foot in let post = Sh.exists (Set.diff post.us xs_and_formals) post in - {xs; foot; post} + let current = Sh.extend_us xs current in + ({xs; foot; post}, current) |> - [%Trace.retn fun {pf} -> pf "@,%a" pp_function_summary] + [%Trace.retn fun {pf} (fs, _) -> pf "@,%a" pp_function_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] ; - let frame = Solver.infer_frame q xs foot in + let xs_in_q = Set.inter xs q.Sh.us in + let xs_in_fv_q = Set.inter xs (Sh.fv q) in + (* Between creation of a summary and its use, the vocabulary of q (q.us) + might have been extended. That means infer_frame would fail, because q + and foot have different vocabulary. This might indicate that the + summary cannot be applied to q, however in the case where + free-variables of q and foot match it is benign. In the case where free + variables match, we temporarily reduce the vocabulary of q to match the + vocabulary of foot. *) + [%Trace.info "xs inter q.us: %a" Var.Set.pp xs_in_q] ; + [%Trace.info "xs inter fv.q %a" Var.Set.pp xs_in_fv_q] ; + let q, add_back = + if Set.is_empty xs_in_fv_q then (Sh.exists xs_in_q q, xs_in_q) + else (q, Var.Set.empty) + in + let frame = + if Set.is_empty xs_in_fv_q then Solver.infer_frame q xs foot else None + in [%Trace.info "frame %a" (Option.pp "%a" pp) frame] ; Option.map ~f:(Sh.star post) frame + |> Option.map ~f:(Sh.extend_us add_back) |> [%Trace.retn fun {pf} r -> match r with None -> pf "None" | Some q -> pf "@,%a" pp q] diff --git a/sledge/src/symbheap/state_domain.mli b/sledge/src/symbheap/state_domain.mli index 725c27261..fb7e044d5 100644 --- a/sledge/src/symbheap/state_domain.mli +++ b/sledge/src/symbheap/state_domain.mli @@ -47,7 +47,11 @@ val apply_summary : function_summary -> t -> t option (* 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 -> t -> function_summary + locals:Var.Set.t + -> formals:Var.Set.t + -> entry:t + -> current:t + -> function_summary * t val post : Var.Set.t -> t -> t val retn : Var.t list -> from_call -> t -> t