From c0c6d65d45a0b479ad4d4b27274b667358a684a4 Mon Sep 17 00:00:00 2001 From: Timotej Kapus Date: Fri, 12 Jul 2019 05:08:42 -0700 Subject: [PATCH] [sledge] Generate and apply summaries Summary: Define a new function summary type and compute it on function return. As an intermediary step also apply the just computed summary to function pre so it can be compared to what was actually computed. Reviewed By: jvillard Differential Revision: D16149833 fbshipit-source-id: b826c17e8 --- sledge/src/control.ml | 31 ++++++++++++++++---- sledge/src/symbheap/domain.ml | 10 ++++++- sledge/src/symbheap/domain.mli | 9 ++++++ sledge/src/symbheap/sh.ml | 3 +- sledge/src/symbheap/solver.ml | 1 + sledge/src/symbheap/state_domain.ml | 44 ++++++++++++++++++++++++++++ sledge/src/symbheap/state_domain.mli | 10 +++++++ 7 files changed, 101 insertions(+), 7 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 10e60b003..67718a847 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -253,6 +253,8 @@ 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 exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump) (return : Llair.jump) throw globals = [%Trace.call fun {pf} -> @@ -264,6 +266,10 @@ let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump) 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 @@ -285,10 +291,11 @@ let pp_st _ = "@[%t@]" (fun fs -> Hashtbl.iteri summary_table ~f:(fun ~key ~data -> Format.fprintf fs "@[%a:@ @[%a@]@]@ " Var.pp key - (List.pp "@," Domain.pp) data ) )] + (List.pp "@," State_domain.pp_function_summary) + data ) )] -let exec_return ~opts stk pre_state (block : Llair.block) exp = - [%Trace.call fun {pf} -> pf "from %a@ " Var.pp block.parent.name.var] +let exec_return ~opts stk pre_state (block : Llair.block) exp globals = + [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var] ; ( match Stack.pop_return stk with | Some (from_call, retn_site, stk) -> @@ -300,7 +307,16 @@ let exec_return ~opts stk pre_state (block : Llair.block) exp = | None, None -> pre_state | _ -> violates Llair.Func.invariant block.parent in - let function_summary = exit_state in + let 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 + ~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 ~data:function_summary ; @@ -311,6 +327,11 @@ let exec_return ~opts stk pre_state (block : Llair.block) exp = 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 @@ -420,7 +441,7 @@ let exec_term : {dst= callee.entry; args; retreating} return throw pgm.globals ) |> Work.seq x ) ) - | Return {exp} -> exec_return ~opts stk state block exp + | 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 diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml index 9dfa200df..cc65b117e 100644 --- a/sledge/src/symbheap/domain.ml +++ b/sledge/src/symbheap/domain.ml @@ -74,7 +74,7 @@ let call ~summaries actuals formals locals globals_vec (entry, current) = [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln] let post locals {caller_entry} (_, current) = - [%Trace.call fun {pf} -> pf ""] + [%Trace.call fun {pf} -> pf "locals: %a" Var.Set.pp locals] ; (caller_entry, State_domain.post locals current) |> @@ -92,3 +92,11 @@ let dnf (entry, current) = 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 apply_summary fs (entry, current) = + 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 24f021e75..5c732874b 100644 --- a/sledge/src/symbheap/domain.mli +++ b/sledge/src/symbheap/domain.mli @@ -28,6 +28,15 @@ val exec_intrinsic : type from_call [@@deriving sexp_of] +(* 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 + +val apply_summary : State_domain.function_summary -> t -> t option val jump : Exp.t list -> Var.t list -> ?temps:Var.Set.t -> t -> t val call : diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 3f8ce82a4..a733226a8 100644 --- a/sledge/src/symbheap/sh.ml +++ b/sledge/src/symbheap/sh.ml @@ -277,7 +277,8 @@ let exists xs q = ; assert ( Set.is_subset xs ~of_:q.us - || Trace.fail "%a" Var.Set.pp (Set.diff xs q.us) ) ; + || Trace.fail "Sh.exists fail xs - q.us:%a" Var.Set.pp + (Set.diff xs q.us) ) ; {q with us= Set.diff q.us xs; xs= Set.union q.xs xs} |> check invariant |> [%Trace.retn fun {pf} -> pf "%a" pp] diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml index 7384a1a63..1d9d14a16 100644 --- a/sledge/src/symbheap/solver.ml +++ b/sledge/src/symbheap/solver.ml @@ -68,6 +68,7 @@ let special_cases xs = function let excise_exp ({us; min; xs} as goal) pure exp = let exp' = Equality.normalize min.cong exp in let exp' = special_cases xs exp' in + [%Trace.info "exp': %a" Exp.pp exp'] ; if Exp.is_true exp' then Some ({goal with pgs= true}, pure) else match single_existential_occurrence xs exp' with diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml index 9186f8b23..a03055cfd 100644 --- a/sledge/src/symbheap/state_domain.ml +++ b/sledge/src/symbheap/state_domain.ml @@ -171,6 +171,50 @@ let resolve_callee lookup ptr _ = | Some callee_name -> lookup callee_name | None -> [] +type function_summary = {xs: Var.Set.t; foot: t; post: t} + +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 = + [%Trace.call fun {pf} -> + pf "formals %a@ entry: %a@ current: %a" Var.Set.pp formals pp entry pp + current] + ; + let foot = Sh.exists locals entry in + let post = Sh.exists locals current in + let foot, subst = Sh.freshen ~wrt:(Set.union foot.us post.us) foot in + let restore_formals q = + Set.fold formals ~init:q ~f:(fun q var -> + let var = Exp.var var in + let renamed_var = Exp.rename var subst in + Sh.and_ (Exp.eq renamed_var var) q ) + in + (* Add back the original formals name *) + let post = Sh.rename subst post in + let foot = restore_formals foot in + let post = restore_formals post in + [%Trace.info "subst: %a" Var.Subst.pp subst] ; + let xs = Set.inter (Sh.fv foot) (Sh.fv post) in + let xs = Set.diff xs formals in + 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} + |> + [%Trace.retn fun {pf} -> pf "@,%a" pp_function_summary] + +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 + [%Trace.info "frame %a" (Option.pp "%a" pp) frame] ; + Option.map ~f:(Sh.star post) frame + |> + [%Trace.retn fun {pf} r -> + match r with None -> pf "None" | Some q -> pf "@,%a" pp q] + let%test_module _ = ( module struct let pp = Format.printf "@.%a@." Sh.pp diff --git a/sledge/src/symbheap/state_domain.mli b/sledge/src/symbheap/state_domain.mli index faf79c4f1..725c27261 100644 --- a/sledge/src/symbheap/state_domain.mli +++ b/sledge/src/symbheap/state_domain.mli @@ -39,6 +39,16 @@ val call : -> t -> t * from_call +type function_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 + +(* 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 + val post : Var.Set.t -> t -> t val retn : Var.t list -> from_call -> t -> t val dnf : t -> t list