[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

@@ -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,15 +264,24 @@ 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
-  List.fold ~init:Work.skip dnf_states ~f:(fun acc state ->
   let locals = dst.parent.locals in
-      caller_state_log :=
+  let domain_call = Domain.call args dst.params locals globals in
-        fst
+  List.fold ~init:Work.skip dnf_states ~f:(fun acc state ->
-          (Domain.call ~summaries:false args dst.params locals globals state)
+      let maybe_summary_post =
-        :: !caller_state_log ;
+        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
+      [%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 args dst.params
+            domain_call ~summaries:opts.function_summaries state
-          locals globals state
           in
           Work.seq acc
             ( match
@@ -280,12 +289,11 @@ let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump)
                   from_call ?throw stk
               with
             | Some stk -> Work.add stk ~prev:block ~retreating state dst
-        | None -> Work.skip ) )
+            | 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
     "@[<v>%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 =
+      let function_summary, exit_state =
-        Domain.create_summary ~locals:block.parent.locals
+        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

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)

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 :

sledge/src/symbheap/state_domain.ml

@@ -177,7 +177,7 @@ let pp_function_summary fs {xs; foot; post} =
   Format.fprintf fs "@[<v>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]

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