[sledge] Account for callees in used-globals analysis

Summary:
Include global variables used in function callees in used globals
analysis.  Also adds support for arbitrary changes to symbolic
state while resolving callees in other analyses.

Reviewed By: jberdine

Differential Revision: D17479352

fbshipit-source-id: e3cd9f179

sledge/src/control.ml

@@ -391,32 +391,31 @@ module Make (Dom : Domain_sig.Dom) = struct
             | Some state -> exec_jump stk state block jump |> Work.seq x
             | None -> x )
     | Call ({callee; args; areturn; return} as call) -> (
-      match
         let lookup name =
           Option.to_list (Llair.Func.find pgm.functions name)
         in
-        Dom.resolve_callee lookup callee state
+        let callees, state = Dom.resolve_callee lookup callee state in
-      with
+        match callees with
-      | [] -> exec_skip_func stk state block areturn return
+        | [] -> exec_skip_func stk state block areturn return
-      | callees ->
+        | callees ->
-          List.fold callees ~init:Work.skip ~f:(fun x callee ->
+            List.fold callees ~init:Work.skip ~f:(fun x callee ->
-              ( match
+                ( match
-                  Dom.exec_intrinsic ~skip_throw:opts.skip_throw state
+                    Dom.exec_intrinsic ~skip_throw:opts.skip_throw state
-                    areturn callee.name.var args
+                      areturn callee.name.var args
-                with
+                  with
-              | Some (Error ()) ->
+                | Some (Error ()) ->
-                  Report.invalid_access_term
+                    Report.invalid_access_term
-                    (Dom.report_fmt_thunk state)
+                      (Dom.report_fmt_thunk state)
-                    block.term ;
+                      block.term ;
-                  Work.skip
+                    Work.skip
-              | Some (Ok state) when Dom.is_false state -> Work.skip
+                | Some (Ok state) when Dom.is_false state -> Work.skip
-              | Some (Ok state) -> exec_jump stk state block return
+                | Some (Ok state) -> exec_jump stk state block return
-              | None when Llair.Func.is_undefined callee ->
+                | None when Llair.Func.is_undefined callee ->
-                  exec_skip_func stk state block areturn return
+                    exec_skip_func stk state block areturn return
-              | None ->
+                | None ->
-                  exec_call opts stk state block {call with callee}
+                    exec_call opts stk state block {call with callee}
-                    pgm.globals )
+                      pgm.globals )
-              |> Work.seq x ) )
+                |> Work.seq x ) )
     | Return {exp} -> exec_return ~opts stk state block exp pgm.globals
     | Throw {exc} ->
         if opts.skip_throw then Work.skip

sledge/src/domain/domain_sig.ml

@@ -44,7 +44,7 @@ module type Dom = sig
   val dnf : t -> t list
 
   val resolve_callee :
-    (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list
+    (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list * t
 
   type summary
 

sledge/src/domain/relation.ml

@@ -107,8 +107,9 @@ module Make (State_domain : State_domain_sig) = struct
   let dnf (entry, current) =
     List.map ~f:(fun c -> (entry, c)) (State_domain.dnf current)
 
-  let resolve_callee f e (_, current) =
+  let resolve_callee f e (entry, current) =
-    State_domain.resolve_callee f e current
+    let callees, current = State_domain.resolve_callee f e current in
+    (callees, (entry, current))
 
   type summary = State_domain.summary
 

sledge/src/domain/unit.ml

@@ -27,10 +27,10 @@ let post _ _ () = ()
 let retn _ _ _ _ = ()
 let dnf () = [()]
 
-let resolve_callee lookup ptr _ =
+let resolve_callee lookup ptr () =
   match Var.of_exp ptr with
-  | Some callee_name -> lookup callee_name
+  | Some callee_name -> (lookup callee_name, ())
-  | None -> []
+  | None -> ([], ())
 
 type summary = unit
 

sledge/src/domain/used_globals.ml

@@ -33,16 +33,14 @@ let exec_kill st _ = st
 let exec_move st _ rhs = used_globals ~init:st rhs
 
 let exec_inst st inst =
-  [%Trace.call fun {pf} -> pf "{%a} %a { ? }" pp st Llair.Inst.pp inst]
+  [%Trace.call fun {pf} -> pf "pre:{%a} %a" pp st Llair.Inst.pp inst]
   ;
   Ok
     (Llair.Inst.fold_exps inst ~init:st ~f:(fun acc e ->
          used_globals ~init:acc e ))
   |>
-  [%Trace.retn fun {pf} res ->
+  [%Trace.retn fun {pf} ->
-    match res with
+    Result.iter ~f:(fun uses -> pf "post:{%a}" pp uses)]
-    | Ok uses -> pf "new uses: %a" pp (Set.diff uses st)
-    | _ -> ()]
 
 let exec_intrinsic ~skip_throw:_ st _ _ actuals =
   List.fold actuals ~init:st ~f:(fun s a -> used_globals ~init:s a)
@@ -54,10 +52,11 @@ type from_call = t [@@deriving sexp_of]
 let call ~summaries:_ actuals _ _ _ _ st =
   (empty, List.fold actuals ~init:st ~f:(fun s a -> used_globals ~init:s a))
 
-let resolve_callee lookup ptr _ =
+let resolve_callee lookup ptr st =
+  let st = used_globals ~init:st ptr in
   match Var.of_exp ptr with
-  | Some callee_name -> lookup callee_name
+  | Some callee_name -> (lookup callee_name, st)
-  | None -> []
+  | None -> ([], st)
 
 (* A function summary is the set of global variables accessed by that
    function and its transitive callees *)

sledge/src/symbheap/state_domain.ml

@@ -155,10 +155,10 @@ let retn formals freturn {areturn; subst; frame} q =
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
-let resolve_callee lookup ptr _ =
+let resolve_callee lookup ptr st =
   match Var.of_exp ptr with
-  | Some callee_name -> lookup callee_name
+  | Some callee_name -> (lookup callee_name, st)
-  | None -> []
+  | None -> ([], st)
 
 type summary = {xs: Var.Set.t; foot: t; post: t}