[sledge] Add data structure to hold summaries

Summary:
On function return add the computed summary (pre/post) condition to a
hashtable.

Reviewed By: jberdine

Differential Revision: D16052136

fbshipit-source-id: 0c5c9bafb

sledge/src/control.ml

@@ -278,7 +278,9 @@ let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump)
   |>
   [%Trace.retn fun {pf} _ -> pf ""]
 
-let exec_return stk pre_state (block : Llair.block) exp =
+let summary_table = Hashtbl.create (module Var)
+
+let exec_return ~opts stk pre_state (block : Llair.block) exp =
   [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var]
   ;
   ( match Stack.pop_return stk with
@@ -291,6 +293,10 @@ let exec_return stk pre_state (block : Llair.block) exp =
         | None, None -> pre_state
         | _ -> violates Llair.Func.invariant block.parent
       in
+      let function_summary = exit_state in
+      if opts.function_summaries then
+        Hashtbl.add_multi summary_table ~key:block.parent.name.var
+          ~data:function_summary ;
       let post_state =
         Domain.post block.parent.locals from_call exit_state
       in
@@ -304,7 +310,11 @@ let exec_return stk pre_state (block : Llair.block) exp =
         | None -> retn_site )
   | None -> Work.skip )
   |>
-  [%Trace.retn fun {pf} _ -> pf ""]
+  [%Trace.retn fun {pf} _ ->
+    pf "@[<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 ) )]
 
 let exec_throw stk pre_state (block : Llair.block) exc =
   [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var]
@@ -405,7 +415,7 @@ let exec_term :
                   {dst= callee.entry; args; retreating}
                   return throw pgm.globals )
             |> Work.seq x ) )
-  | Return {exp} -> exec_return stk state block exp
+  | Return {exp} -> exec_return ~opts stk state block exp
   | Throw {exc} ->
       if opts.skip_throw then Work.skip else exec_throw stk state block exc
   | Unreachable -> Work.skip