[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

@@ -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 _ =
     "@[<v>%t@]" (fun fs ->
         Hashtbl.iteri summary_table ~f:(fun ~key ~data ->
             Format.fprintf fs "@[<v>%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

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)

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 :

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]

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

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 "@[<v>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

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