[sledge] Treat freturn directly in Dom.call

Summary:
Previously it was added to the locals before calling Dom.call, but
this results in the scope of freturn ending too early.

Reviewed By: ngorogiannis

Differential Revision: D17801939

fbshipit-source-id: 739ec8981

sledge/src/control.ml

@@ -281,8 +281,7 @@ module Make (Dom : Domain_sig.Dom) = struct
       if opts.function_summaries then Dom.dnf state else [state]
     in
     let domain_call =
-      Dom.call ~globals ~actuals ~areturn ~formals
+      Dom.call ~globals ~actuals ~areturn ~formals ~freturn ~locals
-        ~locals:(Set.add_option freturn locals)
     in
     List.fold ~init:Work.skip dnf_states ~f:(fun acc state ->
         match
@@ -326,8 +325,7 @@ module Make (Dom : Domain_sig.Dom) = struct
 
   let exec_return ~opts stk pre_state (block : Llair.block) exp =
     let Llair.{name; formals; freturn; locals} = block.parent in
-    [%Trace.call fun {pf} ->
+    [%Trace.call fun {pf} -> pf "from: %a" Reg.pp name.reg]
-      pf "from %a with pre_state %a" Reg.pp name.reg Dom.pp pre_state]
     ;
     let summarize post_state =
       if opts.function_summaries then (
@@ -482,13 +480,14 @@ module Make (Dom : Domain_sig.Dom) = struct
     let entry_points = Config.find_list "entry-points" in
     List.find_map ~f:(Llair.Func.find pgm.functions) entry_points
     |> function
-    | Some {name= {reg}; locals; formals= []; entry} ->
+    | Some {name= {reg}; formals= []; freturn; locals; entry} ->
         Some
           (Work.init
              (fst
                 (Dom.call ~summaries:opts.function_summaries
                    ~globals:(used_globals opts reg) ~actuals:[]
-                   ~areturn:None ~formals:[] ~locals (Dom.init pgm.globals)))
+                   ~areturn:None ~formals:[] ~freturn ~locals
+                   (Dom.init pgm.globals)))
              entry)
     | _ -> None
 

sledge/src/domain/domain_sig.ml

@@ -35,6 +35,7 @@ module type Dom = sig
     -> actuals:Exp.t list
     -> areturn:Reg.t option
     -> formals:Reg.t list
+    -> freturn:Reg.t option
     -> locals:Reg.Set.t
     -> t
     -> t * from_call

sledge/src/domain/relation.ml

@@ -25,8 +25,8 @@ module Make (State_domain : State_domain_sig) = struct
   let embed b = (b, b)
 
   let pp fs (entry, curr) =
-    Format.fprintf fs "@[<v 1> entry: %a@;current:%a@]" State_domain.pp
+    Format.fprintf fs "@[<v>entry: %a@ current: %a@]" State_domain.pp entry
-      entry State_domain.pp curr
+      State_domain.pp curr
 
   let report_fmt_thunk (_, curr) fs = State_domain.pp fs curr
   let init globals = embed (State_domain.init globals)
@@ -68,7 +68,7 @@ module Make (State_domain : State_domain_sig) = struct
 
   let recursion_beyond_bound = State_domain.recursion_beyond_bound
 
-  let call ~summaries ~globals ~actuals ~areturn ~formals ~locals
+  let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals
       (entry, current) =
     [%Trace.call fun {pf} ->
       pf
@@ -80,7 +80,7 @@ module Make (State_domain : State_domain_sig) = struct
     ;
     let caller_current, state_from_call =
       State_domain.call ~summaries ~globals ~actuals ~areturn ~formals
-        ~locals current
+        ~freturn ~locals current
     in
     ( (caller_current, caller_current)
     , {state_from_call; caller_entry= entry} )

sledge/src/domain/unit.ml

@@ -22,8 +22,8 @@ let exec_intrinsic ~skip_throw:_ _ _ _ _ : t option option = None
 
 type from_call = unit [@@deriving compare, equal, sexp]
 
-let call ~summaries:_ ~globals:_ ~actuals:_ ~areturn:_ ~formals:_ ~locals:_
+let call ~summaries:_ ~globals:_ ~actuals:_ ~areturn:_ ~formals:_ ~freturn:_
-    _ =
+    ~locals:_ _ =
   ((), ())
 
 let recursion_beyond_bound = `skip

sledge/src/domain/used_globals.ml

@@ -63,8 +63,8 @@ let exec_intrinsic ~skip_throw:_ st _ intrinsic actuals =
 type from_call = t [@@deriving sexp_of]
 
 (* Set abstract state to bottom (i.e. empty set) at function entry *)
-let call ~summaries:_ ~globals:_ ~actuals ~areturn:_ ~formals:_ ~locals:_ st
+let call ~summaries:_ ~globals:_ ~actuals ~areturn:_ ~formals:_ ~freturn:_
-    =
+    ~locals:_ st =
   (empty, List.fold actuals ~init:st ~f:(fun s a -> used_globals ~init:s a))
 
 let resolve_callee lookup ptr st =

sledge/src/symbheap/sh_domain.ml

@@ -113,7 +113,7 @@ type from_call = {areturn: Var.t option; subst: Var.Subst.t; frame: Sh.t}
 (** Express formula in terms of formals instead of actuals, and enter scope
     of locals: rename formals to fresh vars in formula and actuals, add
     equations between each formal and actual, and quantify fresh vars. *)
-let call ~summaries ~globals ~actuals ~areturn ~formals ~locals q =
+let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
   [%Trace.call fun {pf} ->
     pf
       "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ \
@@ -124,7 +124,7 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~locals q =
   let actuals = List.map ~f:Exp.term actuals in
   let areturn = Option.map ~f:Reg.var areturn in
   let formals = List.map ~f:Reg.var formals in
-  let locals = Reg.Set.vars locals in
+  let locals = Reg.Set.vars (Set.add_option freturn locals) in
   let q', freshen_locals =
     Sh.freshen q ~wrt:(Set.add_list formals locals)
   in